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/uclid_pb_benchmarks/normalized-ooo.burch_dill.6.accl.ucl.opb
MD5SUM	f306f9e77db4c563a096b79aebdedeaa
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	71
Number of bits of the biggest number in a constraint	7
Biggest sum of numbers in a constraint	261
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	23621
Total number of constraints	67526
Number of constraints which are clauses	65126
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	2400
Minimum length of a constraint	1
Maximum length of a constraint	13
Trace number 5604

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        835500 kB
Buffers:         34900 kB
Cached:         123648 kB
SwapCached:       2476 kB
Active:          57140 kB
Inactive:       106764 kB
HighTotal:      131008 kB
HighFree:         4284 kB
LowTotal:       903652 kB
LowFree:        831216 kB
SwapTotal:     2097892 kB
SwapFree:      2095416 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            29680 kB
Committed_AS:    63616 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:07:13 (client local time) WITH STATUS 0 IN 1200.31 SECONDS
stats: 4059 7 1200.31 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 67525 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: #########################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[67505]---> BDD-cost:    1
c ---[67500]---> BDD-cost:    1
c ---[67486]---> BDD-cost:    1
c ---[67478]---> BDD-cost:    1
c ---[67434]---> BDD-cost:    1
c ---[67426]---> BDD-cost:    1
c ---[67412]---> BDD-cost:    1
c ---[67368]---> BDD-cost:    1
c ---[67354]---> BDD-cost:    1
c ---[67280]---> BDD-cost:    1
c ---[67272]---> BDD-cost:    1
c ---[67258]---> BDD-cost:    1
c ---[67217]---> BDD-cost:    1
c ---[67179]---> BDD-cost:    1
c ---[67159]---> BDD-cost:    1
c ---[67055]---> BDD-cost:    1
c ---[67047]---> BDD-cost:    1
c ---[67033]---> BDD-cost:    1
c ---[66992]---> BDD-cost:    1
c ---[66954]---> BDD-cost:    1
c ---[66916]---> BDD-cost:    1
c ---[66890]---> BDD-cost:    1
c ---[66753]---> BDD-cost:    1
c ---[66745]---> BDD-cost:    1
c ---[66731]---> BDD-cost:    1
c ---[66690]---> BDD-cost:    1
c ---[66652]---> BDD-cost:    1
c ---[66614]---> BDD-cost:    1
c ---[66576]---> BDD-cost:    1
c ---[66544]---> BDD-cost:    1
c ---[66371]---> BDD-cost:    1
c ---[66363]---> BDD-cost:    1
c ---[66349]---> BDD-cost:    1
c ---[66308]---> BDD-cost:    1
c ---[66270]---> BDD-cost:    1
c ---[66232]---> BDD-cost:    1
c ---[66194]---> BDD-cost:    1
c ---[66156]---> BDD-cost:    1
c ---[66118]---> BDD-cost:    1
c ---[65879]---> BDD-cost:    1
c ---[65856]---> BDD-cost:    1
c ---[65848]---> BDD-cost:    1
c ---[65819]---> BDD-cost:    1
c ---[65811]---> BDD-cost:    1
c ---[65797]---> BDD-cost:    1
c ---[65774]---> BDD-cost:    1
c ---[65766]---> BDD-cost:    1
c ---[65758]---> BDD-cost:    1
c ---[65738]---> BDD-cost:    1
c ---[65706]---> BDD-cost:    1
c ---[65698]---> BDD-cost:    1
c ---[65690]---> BDD-cost:    1
c ---[65682]---> BDD-cost:    1
c ---[65656]---> BDD-cost:    1
c ---[65633]---> BDD-cost:    1
c ---[65625]---> BDD-cost:    1
c ---[65617]---> BDD-cost:    1
c ---[65609]---> BDD-cost:    1
c ---[65601]---> BDD-cost:    1
c ---[65569]---> BDD-cost:    1
c ---[65537]---> BDD-cost:    1
c ---[65529]---> BDD-cost:    1
c ---[65521]---> BDD-cost:    1
c ---[65513]---> BDD-cost:    1
c ---[65505]---> BDD-cost:    1
c ---[65497]---> BDD-cost:    1
c ---[65459]---> BDD-cost:    1
c ---[65436]---> BDD-cost:    1
c ---[65428]---> BDD-cost:    1
c ---[65420]---> BDD-cost:    1
c ---[65412]---> BDD-cost:    1
c ---[65404]---> BDD-cost:    1
c ---[65396]---> BDD-cost:    1
c ---[65388]---> BDD-cost:    1
c ---[65344]---> BDD-cost:    1
c ---[65312]---> BDD-cost:    1
c ---[65304]---> BDD-cost:    1
c ---[65296]---> BDD-cost:    1
c ---[65288]---> BDD-cost:    1
c ---[65280]---> BDD-cost:    1
c ---[65272]---> BDD-cost:    1
c ---[65264]---> BDD-cost:    1
c ---[65256]---> BDD-cost:    1
c ---[65206]---> BDD-cost:    1
c ---[65183]---> BDD-cost:    1
c ---[65175]---> BDD-cost:    1
c ---[65167]---> BDD-cost:    1
c ---[65159]---> BDD-cost:    1
c ---[65151]---> BDD-cost:    1
c ---[65143]---> BDD-cost:    1
c ---[65135]---> BDD-cost:    1
c ---[65127]---> BDD-cost:    1
c ---[65119]---> BDD-cost:    1
c ---[65063]---> BDD-cost:    1
c ---[65031]---> BDD-cost:    1
c ---[65023]---> BDD-cost:    1
c ---[65015]---> BDD-cost:    1
c ---[65007]---> BDD-cost:    1
c ---[64999]---> BDD-cost:    1
c ---[64991]---> BDD-cost:    1
c ---[64983]---> BDD-cost:    1
c ---[64975]---> BDD-cost:    1
c ---[64967]---> BDD-cost:    1
c ---[64959]---> BDD-cost:    1
c ---[64897]---> BDD-cost:    1
c ---[64874]---> BDD-cost:    1
c ---[64866]---> BDD-cost:    1
c ---[64858]---> BDD-cost:    1
c ---[64850]---> BDD-cost:    1
c ---[64842]---> BDD-cost:    1
c ---[64834]---> BDD-cost:    1
c ---[64826]---> BDD-cost:    1
c ---[64818]---> BDD-cost:    1
c ---[64810]---> BDD-cost:    1
c ---[64802]---> BDD-cost:    1
c ---[64794]---> BDD-cost:    1
c ---[64726]---> BDD-cost:    1
c ---[64697]---> BDD-cost:    1
c ---[64677]---> BDD-cost:    1
c ---[64660]---> BDD-cost:    1
c ---[64643]---> BDD-cost:    1
c ---[64626]---> BDD-cost:    1
c ---[64609]---> BDD-cost:    1
c ---[64592]---> BDD-cost:    1
c ---[64242]---> BDD-cost:    1
c ---[64234]---> BDD-cost:    1
c ---[64163]---> BDD-cost:    1
c ---[64092]---> BDD-cost:    1
c ---[64021]---> BDD-cost:    1
c ---[63950]---> BDD-cost:    1
c ---[63879]---> BDD-cost:    1
c ---[63815]---> BDD-cost:    1
c ---[63807]---> BDD-cost:    1
c ---[63802]---> BDD-cost:    1
c ---[63800]---> BDD-cost:    1
c ---[63786]---> BDD-cost:    1
c ---[63781]---> BDD-cost:    1
c ---[63776]---> BDD-cost:    1
c ---[63771]---> BDD-cost:    1
c ---[63766]---> BDD-cost:    1
c ---[63761]---> BDD-cost:    1
c ---[63756]---> BDD-cost:    1
c ---[63751]---> BDD-cost:    1
c ---[63746]---> BDD-cost:    1
c ---[63741]---> BDD-cost:    1
c ---[63736]---> BDD-cost:    1
c ---[63731]---> BDD-cost:    1
c ---[63648]---> BDD-cost:    1
c ---[63637]---> BDD-cost:    1
c ---[63596]---> BDD-cost:    1
c ---[63528]---> BDD-cost:    1
c ---[63433]---> BDD-cost:    1
c ---[63311]---> BDD-cost:    1
c ---[63174]---> BDD-cost:    1
c ---[63067]---> BDD-cost:    1
c ---[63014]---> BDD-cost:    1
c ---[63000]---> BDD-cost:    1
c ---[62983]---> BDD-cost:    1
c ---[62963]---> BDD-cost:    1
c ---[62940]---> BDD-cost:    1
c ---[62914]---> BDD-cost:    1
c ---[62885]---> BDD-cost:    1
c ---[62331]---> BDD-cost:    1
c ---[62128]---> BDD-cost:    1
c ---[62120]---> BDD-cost:    1
c ---[62112]---> BDD-cost:    1
c ---[62104]---> BDD-cost:    1
c ---[62096]---> BDD-cost:    1
c ---[62088]---> BDD-cost:    1
c ---[62080]---> BDD-cost:    1
c ---[62072]---> BDD-cost:    1
c ---[62064]---> BDD-cost:    1
c ---[62056]---> BDD-cost:    1
c ---[62048]---> BDD-cost:    1
c ---[62040]---> BDD-cost:    1
c ---[61951]---> BDD-cost:    1
c ---[61928]---> BDD-cost:    1
c ---[61920]---> BDD-cost:    1
c ---[61912]---> BDD-cost:    1
c ---[61904]---> BDD-cost:    1
c ---[61896]---> BDD-cost:    1
c ---[61888]---> BDD-cost:    1
c ---[61784]---> BDD-cost:    1
c ---[61776]---> BDD-cost:    1
c ---[61768]---> BDD-cost:    1
c ---[61760]---> BDD-cost:    1
c ---[61752]---> BDD-cost:    1
c ---[61744]---> BDD-cost:    1
c ---[61736]---> BDD-cost:    1
c ---[61728]---> BDD-cost:    1
c ---[61720]---> BDD-cost:    1
c ---[61712]---> BDD-cost:    1
c ---[61704]---> BDD-cost:    1
c ---[61696]---> BDD-cost:    1
c ---[61685]---> BDD-cost:    1
c ---[61599]---> BDD-cost:    1
c ---[61576]---> BDD-cost:    1
c ---[61556]---> BDD-cost:    1
c ---[61440]---> BDD-cost:    1
c ---[61369]---> BDD-cost:    1
c ---[61298]---> BDD-cost:    1
c ---[61227]---> BDD-cost:    1
c ---[61156]---> BDD-cost:    1
c ---[61085]---> BDD-cost:    1
c ---[61014]---> BDD-cost:    1
c ---[60943]---> BDD-cost:    1
c ---[60872]---> BDD-cost:    1
c ---[60801]---> BDD-cost:    1
c ---[60730]---> BDD-cost:    1
c ---[60659]---> BDD-cost:    1
c ---[60582]---> BDD-cost:    1
c ---[60457]---> BDD-cost:    1
c ---[60401]---> BDD-cost:    1
c ---[60384]---> BDD-cost:    1
c ---[60367]---> BDD-cost:    1
c ---[60350]---> BDD-cost:    1
c ---[60333]---> BDD-cost:    1
c ---[60316]---> BDD-cost:    1
c ---[60299]---> BDD-cost:    1
c ---[60282]---> BDD-cost:    1
c ---[60265]---> BDD-cost:    1
c ---[60248]---> BDD-cost:    1
c ---[60231]---> BDD-cost:    1
c ---[60214]---> BDD-cost:    1
c ---[60197]---> BDD-cost:    1
c ---[60048]---> BDD-cost:    1
c ---[59944]---> BDD-cost:    1
c ---[59918]---> BDD-cost:    1
c ---[59913]---> BDD-cost:    1
c ---[59908]---> BDD-cost:    1
c ---[59903]---> BDD-cost:    1
c ---[59883]---> BDD-cost:    1
c ---[59869]---> BDD-cost:    1
c ---[59837]---> BDD-cost:    1
c ---[59751]---> BDD-cost:    1
c ---[59542]---> BDD-cost:    1
c ---[59483]---> BDD-cost:    1
c ---[59199]---> BDD-cost:    1
c ---[59176]---> BDD-cost:    1
c ---[59153]---> BDD-cost:    1
c ---[59130]---> BDD-cost:    1
c ---[59107]---> BDD-cost:    1
c ---[59084]---> BDD-cost:    1
c ---[59061]---> BDD-cost:    1
c ---[59038]---> BDD-cost:    1
c ---[59015]---> BDD-cost:    1
c ---[58992]---> BDD-cost:    1
c ---[58969]---> BDD-cost:    1
c ---[58946]---> BDD-cost:    1
c ---[58923]---> BDD-cost:    1
c ---[58702]---> BDD-cost:    1
c ---[58586]---> BDD-cost:    1
c ---[58554]---> BDD-cost:    1
c ---[58549]---> BDD-cost:    1
c ---[58544]---> BDD-cost:    1
c ---[58539]---> BDD-cost:    1
c ---[58534]---> BDD-cost:    1
c ---[58508]---> BDD-cost:    1
c ---[58494]---> BDD-cost:    1
c ---[58474]---> BDD-cost:    1
c ---[58430]---> BDD-cost:    1
c ---[58302]---> BDD-cost:    1
c ---[58117]---> BDD-cost:    1
c ---[57800]---> BDD-cost:    1
c ---[57732]---> BDD-cost:    1
c ---[57460]---> BDD-cost:    1
c ---[57056]---> BDD-cost:    1
c ---[57027]---> BDD-cost:    1
c ---[56998]---> BDD-cost:    1
c ---[56969]---> BDD-cost:    1
c ---[56940]---> BDD-cost:    1
c ---[56911]---> BDD-cost:    1
c ---[56882]---> BDD-cost:    1
c ---[56853]---> BDD-cost:    1
c ---[56824]---> BDD-cost:    1
c ---[56795]---> BDD-cost:    1
c ---[56766]---> BDD-cost:    1
c ---[56737]---> BDD-cost:    1
c ---[56708]---> BDD-cost:    1
c ---[56415]---> BDD-cost:    1
c ---[56287]---> BDD-cost:    1
c ---[56249]---> BDD-cost:    1
c ---[56244]---> BDD-cost:    1
c ---[56239]---> BDD-cost:    1
c ---[56234]---> BDD-cost:    1
c ---[56229]---> BDD-cost:    1
c ---[56224]---> BDD-cost:    1
c ---[56192]---> BDD-cost:    1
c ---[56178]---> BDD-cost:    1
c ---[56158]---> BDD-cost:    1
c ---[56132]---> BDD-cost:    1
c ---[56076]---> BDD-cost:    1
c ---[55891]---> BDD-cost:    1
c ---[55664]---> BDD-cost:    1
c ---[55377]---> BDD-cost:    1
c ---[54895]---> BDD-cost:    1
c ---[54815]---> BDD-cost:    1
c ---[54519]---> BDD-cost:    1
c ---[54124]---> BDD-cost:    1
c ---[53546]---> BDD-cost:    1
c ---[53511]---> BDD-cost:    1
c ---[53476]---> BDD-cost:    1
c ---[53441]---> BDD-cost:    1
c ---[53406]---> BDD-cost:    1
c ---[53371]---> BDD-cost:    1
c ---[53336]---> BDD-cost:    1
c ---[53301]---> BDD-cost:    1
c ---[53266]---> BDD-cost:    1
c ---[53231]---> BDD-cost:    1
c ---[53196]---> BDD-cost:    1
c ---[53161]---> BDD-cost:    1
c ---[53126]---> BDD-cost:    1
c ---[52761]---> BDD-cost:    1
c ---[52621]---> BDD-cost:    1
c ---[52577]---> BDD-cost:    1
c ---[52572]---> BDD-cost:    1
c ---[52567]---> BDD-cost:    1
c ---[52562]---> BDD-cost:    1
c ---[52557]---> BDD-cost:    1
c ---[52552]---> BDD-cost:    1
c ---[52547]---> BDD-cost:    1
c ---[52509]---> BDD-cost:    1
c ---[52495]---> BDD-cost:    1
c ---[52475]---> BDD-cost:    1
c ---[52449]---> BDD-cost:    1
c ---[52417]---> BDD-cost:    1
c ---[52349]---> BDD-cost:    1
c ---[52095]---> BDD-cost:    1
c ---[51826]---> BDD-cost:    1
c ---[51485]---> BDD-cost:    1
c ---[51036]---> BDD-cost:    1
c ---[50353]---> BDD-cost:    1
c ---[50261]---> BDD-cost:    1
c ---[49941]---> BDD-cost:    1
c ---[49510]---> BDD-cost:    1
c ---[48941]---> BDD-cost:    1
c ---[48165]---> BDD-cost:    1
c ---[48124]---> BDD-cost:    1
c ---[48083]---> BDD-cost:    1
c ---[48042]---> BDD-cost:    1
c ---[48001]---> BDD-cost:    1
c ---[47960]---> BDD-cost:    1
c ---[47919]---> BDD-cost:    1
c ---[47878]---> BDD-cost:    1
c ---[47837]---> BDD-cost:    1
c ---[47796]---> BDD-cost:    1
c ---[47755]---> BDD-cost:    1
c ---[47714]---> BDD-cost:    1
c ---[47673]---> BDD-cost:    1
c ---[47236]---> BDD-cost:    1
c ---[47084]---> BDD-cost:    1
c ---[46869]---> BDD-cost:    1
c ---[46822]---> BDD-cost:    1
c ---[46775]---> BDD-cost:    1
c ---[46728]---> BDD-cost:    1
c ---[46681]---> BDD-cost:    1
c ---[46634]---> BDD-cost:    1
c ---[46587]---> BDD-cost:    1
c ---[46540]---> BDD-cost:    1
c ---[46493]---> BDD-cost:    1
c ---[46446]---> BDD-cost:    1
c ---[46399]---> BDD-cost:    1
c ---[46352]---> BDD-cost:    1
c ---[46341]---> BDD-cost:    1
c ---[46333]---> BDD-cost:    1
c ---[46328]---> BDD-cost:    1
c ---[46323]---> BDD-cost:    1
c ---[46318]---> BDD-cost:    1
c ---[46313]---> BDD-cost:    1
c ---[46161]---> BDD-cost:    1
c ---[46159]---> BDD-cost:    1
c ---[46157]---> BDD-cost:    1
c ---[46155]---> BDD-cost:    1
c ---[46150]---> BDD-cost:    1
c ---[46145]---> BDD-cost:    1
c ---[46143]---> BDD-cost:    1
c ---[46120]---> BDD-cost:    1
c ---[46118]---> BDD-cost:    1
c ---[46116]---> BDD-cost:    1
c ---[46114]---> BDD-cost:    1
c ---[46109]---> BDD-cost:    1
c ---[46104]---> BDD-cost:    1
c ---[46102]---> BDD-cost:    1
c ---[46070]---> BDD-cost:    1
c ---[46050]---> BDD-cost:    1
c ---[46048]---> BDD-cost:    1
c ---[46046]---> BDD-cost:    1
c ---[46041]---> BDD-cost:    1
c ---[46036]---> BDD-cost:    1
c ---[46034]---> BDD-cost:    1
c ---[46014]---> BDD-cost:    1
c ---[46012]---> BDD-cost:    1
c ---[46010]---> BDD-cost:    1
c ---[46005]---> BDD-cost:    1
c ---[46000]---> BDD-cost:    1
c ---[45998]---> BDD-cost:    1
c ---[45969]---> BDD-cost:    1
c ---[45931]---> BDD-cost:    1
c ---[45929]---> BDD-cost:    1
c ---[45924]---> BDD-cost:    1
c ---[45919]---> BDD-cost:    1
c ---[45917]---> BDD-cost:    1
c ---[45900]---> BDD-cost:    1
c ---[45898]---> BDD-cost:    1
c ---[45893]---> BDD-cost:    1
c ---[45888]---> BDD-cost:    1
c ---[45886]---> BDD-cost:    1
c ---[45860]---> BDD-cost:    1
c ---[45801]---> BDD-cost:    1
c ---[45796]---> BDD-cost:    1
c ---[45791]---> BDD-cost:    1
c ---[45789]---> BDD-cost:    1
c ---[45775]---> BDD-cost:    1
c ---[45770]---> BDD-cost:    1
c ---[45765]---> BDD-cost:    1
c ---[45763]---> BDD-cost:    1
c ---[45740]---> BDD-cost:    1
c ---[45654]---> BDD-cost:    1
c ---[45649]---> BDD-cost:    1
c ---[45647]---> BDD-cost:    1
c ---[45633]---> BDD-cost:    1
c ---[45628]---> BDD-cost:    1
c ---[45626]---> BDD-cost:    1
c ---[45606]---> BDD-cost:    1
c ---[45571]---> BDD-cost:    1
c ---[45350]---> BDD-cost:    1
c ---[45102]---> BDD-cost:    1
c ---[44812]---> BDD-cost:    1
c ---[44444]---> BDD-cost:    1
c ---[43959]---> BDD-cost:    1
c ---[43357]---> BDD-cost:    1
c ---[42617]---> BDD-cost:    1
c ---[42615]---> BDD-cost:    1
c ---[42613]---> BDD-cost:    1
c ---[42611]---> BDD-cost:    1
c ---[42609]---> BDD-cost:    1
c ---[42604]---> BDD-cost:    1
c ---[42599]---> BDD-cost:    1
c ---[42597]---> BDD-cost:    1
c ---[42460]---> BDD-cost:    1
c ---[42362]---> BDD-cost:    1
c ---[42030]---> BDD-cost:    1
c ---[41581]---> BDD-cost:    1
c ---[40988]---> BDD-cost:    1
c ---[40251]---> BDD-cost:    1
c ---[39358]---> BDD-cost:    1
c ---[39356]---> BDD-cost:    1
c ---[39354]---> BDD-cost:    1
c ---[39352]---> BDD-cost:    1
c ---[39350]---> BDD-cost:    1
c ---[39345]---> BDD-cost:    1
c ---[39340]---> BDD-cost:    1
c ---[39338]---> BDD-cost:    1
c ---[39297]---> BDD-cost:    1
c ---[39106]---> BDD-cost:    1
c ---[39101]---> BDD-cost:    1
c ---[39096]---> BDD-cost:    1
c ---[39091]---> BDD-cost:    1
c ---[39053]---> BDD-cost:    1
c ---[38847]---> BDD-cost:    1
c ---[38842]---> BDD-cost:    1
c ---[38837]---> BDD-cost:    1
c ---[38805]---> BDD-cost:    1
c ---[38593]---> BDD-cost:    1
c ---[38588]---> BDD-cost:    1
c ---[38562]---> BDD-cost:    1
c ---[38350]---> BDD-cost:    1
c ---[38330]---> BDD-cost:    1
c ---[38073]---> BDD-cost:    1
c ---[38041]---> BDD-cost:    1
c ---[37994]---> BDD-cost:    1
c ---[37932]---> BDD-cost:    1
c ---[37861]---> BDD-cost:    1
c ---[37859]---> BDD-cost:    1
c ---[37857]---> BDD-cost:    1
c ---[37855]---> BDD-cost:    1
c ---[37853]---> BDD-cost:    1
c ---[37851]---> BDD-cost:    1
c ---[37849]---> BDD-cost:    1
c ---[37418]---> BDD-cost:    1
c ---[37383]---> BDD-cost:    1
c ---[37318]---> BDD-cost:    1
c ---[37256]---> BDD-cost:    1
c ---[37197]---> BDD-cost:    1
c ---[37141]---> BDD-cost:    1
c ---[37088]---> BDD-cost:    1
c ---[36825]---> BDD-cost:    1
c ---[36802]---> BDD-cost:    1
c ---[36788]---> BDD-cost:    1
c ---[36774]---> BDD-cost:    1
c ---[36760]---> BDD-cost:    1
c ---[36746]---> BDD-cost:    1
c ---[36732]---> BDD-cost:    1
c ---[36718]---> BDD-cost:    1
c ---[36662]---> BDD-cost:    1
c ---[36396]---> BDD-cost:    1
c ---[36310]---> BDD-cost:    1
c ---[36299]---> BDD-cost:    1
c ---[36285]---> BDD-cost:    1
c ---[36271]---> BDD-cost:    1
c ---[36257]---> BDD-cost:    1
c ---[36243]---> BDD-cost:    1
c ---[36229]---> BDD-cost:    1
c ---[36215]---> BDD-cost:    1
c ---[36201]---> BDD-cost:    1
c ---[36187]---> BDD-cost:    1
c ---[36173]---> BDD-cost:    1
c ---[36159]---> BDD-cost:    1
c ---[36142]---> BDD-cost:    1
c ---[35993]---> BDD-cost:    1
c ---[35838]---> BDD-cost:    1
c ---[35830]---> BDD-cost:    1
c ---[35825]---> BDD-cost:    1
c ---[35820]---> BDD-cost:    1
c ---[35800]---> BDD-cost:    1
c ---[35786]---> BDD-cost:    1
c ---[35766]---> BDD-cost:    1
c ---[35746]---> BDD-cost:    1
c ---[35726]---> BDD-cost:    1
c ---[35706]---> BDD-cost:    1
c ---[35686]---> BDD-cost:    1
c ---[35672]---> BDD-cost:    1
c ---[35604]---> BDD-cost:    1
c ---[35359]---> BDD-cost:    1
c ---[35036]---> BDD-cost:    1
c ---[34953]---> BDD-cost:    1
c ---[34777]---> BDD-cost:    1
c ---[34760]---> BDD-cost:    1
c ---[34740]---> BDD-cost:    1
c ---[34720]---> BDD-cost:    1
c ---[34700]---> BDD-cost:    1
c ---[34680]---> BDD-cost:    1
c ---[34660]---> BDD-cost:    1
c ---[34640]---> BDD-cost:    1
c ---[34620]---> BDD-cost:    1
c ---[34600]---> BDD-cost:    1
c ---[34580]---> BDD-cost:    1
c ---[34560]---> BDD-cost:    1
c ---[34537]---> BDD-cost:    1
c ---[34316]---> BDD-cost:    1
c ---[34149]---> BDD-cost:    1
c ---[34141]---> BDD-cost:    1
c ---[34136]---> BDD-cost:    1
c ---[34131]---> BDD-cost:    1
c ---[34126]---> BDD-cost:    1
c ---[34100]---> BDD-cost:    1
c ---[34086]---> BDD-cost:    1
c ---[34066]---> BDD-cost:    1
c ---[34040]---> BDD-cost:    1
c ---[34014]---> BDD-cost:    1
c ---[33988]---> BDD-cost:    1
c ---[33962]---> BDD-cost:    1
c ---[33948]---> BDD-cost:    1
c ---[33928]---> BDD-cost:    1
c ---[33848]---> BDD-cost:    1
c ---[33522]---> BDD-cost:    1
c ---[33277]---> BDD-cost:    1
c ---[32777]---> BDD-cost:    1
c ---[32682]---> BDD-cost:    1
c ---[32509]---> BDD-cost:    1
c ---[32219]---> BDD-cost:    1
c ---[32196]---> BDD-cost:    1
c ---[32170]---> BDD-cost:    1
c ---[32144]---> BDD-cost:    1
c ---[32118]---> BDD-cost:    1
c ---[32092]---> BDD-cost:    1
c ---[32066]---> BDD-cost:    1
c ---[32040]---> BDD-cost:    1
c ---[32014]---> BDD-cost:    1
c ---[31988]---> BDD-cost:    1
c ---[31962]---> BDD-cost:    1
c ---[31936]---> BDD-cost:    1
c ---[31907]---> BDD-cost:    1
c ---[31614]---> BDD-cost:    1
c ---[31435]---> BDD-cost:    1
c ---[31427]---> BDD-cost:    1
c ---[31422]---> BDD-cost:    1
c ---[31417]---> BDD-cost:    1
c ---[31412]---> BDD-cost:    1
c ---[31407]---> BDD-cost:    1
c ---[31375]---> BDD-cost:    1
c ---[31361]---> BDD-cost:    1
c ---[31341]---> BDD-cost:    1
c ---[31315]---> BDD-cost:    1
c ---[31283]---> BDD-cost:    1
c ---[31251]---> BDD-cost:    1
c ---[31219]---> BDD-cost:    1
c ---[31205]---> BDD-cost:    1
c ---[31185]---> BDD-cost:    1
c ---[31159]---> BDD-cost:    1
c ---[31067]---> BDD-cost:    1
c ---[30648]---> BDD-cost:    1
c ---[30367]---> BDD-cost:    1
c ---[29948]---> BDD-cost:    1
c ---[29238]---> BDD-cost:    1
c ---[29131]---> BDD-cost:    1
c ---[28934]---> BDD-cost:    1
c ---[28647]---> BDD-cost:    1
c ---[28219]---> BDD-cost:    1
c ---[28190]---> BDD-cost:    1
c ---[28158]---> BDD-cost:    1
c ---[28126]---> BDD-cost:    1
c ---[28094]---> BDD-cost:    1
c ---[28062]---> BDD-cost:    1
c ---[28030]---> BDD-cost:    1
c ---[27998]---> BDD-cost:    1
c ---[27966]---> BDD-cost:    1
c ---[27934]---> BDD-cost:    1
c ---[27902]---> BDD-cost:    1
c ---[27870]---> BDD-cost:    1
c ---[27835]---> BDD-cost:    1
c ---[27470]---> BDD-cost:    1
c ---[27279]---> BDD-cost:    1
c ---[27151]---> BDD-cost:    1
c ---[27113]---> BDD-cost:    1
c ---[27075]---> BDD-cost:    1
c ---[27037]---> BDD-cost:    1
c ---[26999]---> BDD-cost:    1
c ---[26961]---> BDD-cost:    1
c ---[26923]---> BDD-cost:    1
c ---[26885]---> BDD-cost:    1
c ---[26847]---> BDD-cost:    1
c ---[26809]---> BDD-cost:    1
c ---[26771]---> BDD-cost:    1
c ---[26733]---> BDD-cost:    1
c ---[26689]---> BDD-cost:    1
c ---[26663]---> BDD-cost:    1
c ---[26658]---> BDD-cost:    1
c ---[26653]---> BDD-cost:    1
c ---[26648]---> BDD-cost:    1
c ---[26397]---> BDD-cost:    1
c ---[26395]---> BDD-cost:    1
c ---[26393]---> BDD-cost:    1
c ---[26391]---> BDD-cost:    1
c ---[26377]---> BDD-cost:    1
c ---[26375]---> BDD-cost:    1
c ---[26373]---> BDD-cost:    1
c ---[26371]---> BDD-cost:    1
c ---[26348]---> BDD-cost:    1
c ---[26268]---> BDD-cost:    1
c ---[26266]---> BDD-cost:    1
c ---[26264]---> BDD-cost:    1
c ---[26253]---> BDD-cost:    1
c ---[26251]---> BDD-cost:    1
c ---[26249]---> BDD-cost:    1
c ---[26229]---> BDD-cost:    1
c ---[26149]---> BDD-cost:    1
c ---[26147]---> BDD-cost:    1
c ---[26139]---> BDD-cost:    1
c ---[26137]---> BDD-cost:    1
c ---[26120]---> BDD-cost:    1
c ---[26040]---> BDD-cost:    1
c ---[26035]---> BDD-cost:    1
c ---[26021]---> BDD-cost:    1
c ---[25908]---> BDD-cost:    1
c ---[25705]---> BDD-cost:    1
c ---[25229]---> BDD-cost:    1
c ---[24912]---> BDD-cost:    1
c ---[24439]---> BDD-cost:    1
c ---[23813]---> BDD-cost:    1
c ---[23016]---> BDD-cost:    1
c ---[23014]---> BDD-cost:    1
c ---[23012]---> BDD-cost:    1
c ---[23010]---> BDD-cost:    1
c ---[23008]---> BDD-cost:    1
c ---[22838]---> BDD-cost:    1
c ---[22722]---> BDD-cost:    1
c ---[22501]---> BDD-cost:    1
c ---[22178]---> BDD-cost:    1
c ---[21753]---> BDD-cost:    1
c ---[21217]---> BDD-cost:    1
c ---[21215]---> BDD-cost:    1
c ---[21213]---> BDD-cost:    1
c ---[21211]---> BDD-cost:    1
c ---[21209]---> BDD-cost:    1
c ---[21177]---> BDD-cost:    1
c ---[20827]---> BDD-cost:    1
c ---[20822]---> BDD-cost:    1
c ---[20817]---> BDD-cost:    1
c ---[20782]---> BDD-cost:    1
c ---[20420]---> BDD-cost:    1
c ---[20415]---> BDD-cost:    1
c ---[20386]---> BDD-cost:    1
c ---[20015]---> BDD-cost:    1
c ---[19992]---> BDD-cost:    1
c ---[19603]---> BDD-cost:    1
c ---[19550]---> BDD-cost:    1
c ---[19188]---> BDD-cost:    1
c ---[18913]---> BDD-cost:    1
c ---[18674]---> BDD-cost:    1
c ---[18471]---> BDD-cost:    1
c ---[18439]---> BDD-cost:    1
c ---[17906]---> BDD-cost:    1
c ---[17724]---> BDD-cost:    1
c ---[17566]---> BDD-cost:    1
c ---[17432]---> BDD-cost:    1
c ---[17322]---> BDD-cost:    1
c ---[17236]---> BDD-cost:    1
c ---[16988]---> BDD-cost:    1
c ---[16734]---> BDD-cost:    1
c ---[16531]---> BDD-cost:    1
c ---[16346]---> BDD-cost:    1
c ---[16317]---> BDD-cost:    1
c ---[15946]---> BDD-cost:    1
c ---[15743]---> BDD-cost:    1
c ---[15564]---> BDD-cost:    1
c ---[15409]---> BDD-cost:    1
c ---[15278]---> BDD-cost:    1
c ---[15171]---> BDD-cost:    1
c ---[14911]---> BDD-cost:    1
c ---[14642]---> BDD-cost:    1
c ---[14430]---> BDD-cost:    1
c ---[14404]---> BDD-cost:    1
c ---[14069]---> BDD-cost:    1
c ---[13845]---> BDD-cost:    1
c ---[13645]---> BDD-cost:    1
c ---[13469]---> BDD-cost:    1
c ---[13317]---> BDD-cost:    1
c ---[13189]---> BDD-cost:    1
c ---[12917]---> BDD-cost:    1
c ---[12633]---> BDD-cost:    1
c ---[12610]---> BDD-cost:    1
c ---[12302]---> BDD-cost:    1
c ---[12057]---> BDD-cost:    1
c ---[11836]---> BDD-cost:    1
c ---[11639]---> BDD-cost:    1
c ---[11466]---> BDD-cost:    1
c ---[11317]---> BDD-cost:    1
c ---[11033]---> BDD-cost:    1
c ---[11013]---> BDD-cost:    1
c ---[10672]---> BDD-cost:    1
c ---[10406]---> BDD-cost:    1
c ---[10164]---> BDD-cost:    1
c ---[9946]---> BDD-cost:    1
c ---[9752]---> BDD-cost:    1
c ---[9582]---> BDD-cost:    1
c ---[9289]---> BDD-cost:    1
c ---[9266]---> BDD-cost:    1
c ---[8844]---> BDD-cost:    1
c ---[8521]---> BDD-cost:    1
c ---[8222]---> BDD-cost:    1
c ---[7947]---> BDD-cost:    1
c ---[7696]---> BDD-cost:    1
c ---[7328]---> BDD-cost:    1
c ---[7320]---> BDD-cost:    1
c ---[7294]---> BDD-cost:    1
c ---[7271]---> BDD-cost:    1
c ---[7221]---> BDD-cost:    1
c ---[7168]---> BDD-cost:    1
c ---[7151]---> BDD-cost:    1
c ---[7131]---> BDD-cost:    1
c ---[7108]---> BDD-cost:    1
c ---[7082]---> BDD-cost:    1
c ---[7053]---> BDD-cost:    1
c ---[7015]---> BDD-cost:    1
c ---[6998]---> BDD-cost:    1
c ---[6978]---> BDD-cost:    1
c ---[6955]---> BDD-cost:    1
c ---[6929]---> BDD-cost:    1
c ---[4908]---> BDD-cost:    1
c ---[4783]---> BDD-cost:    1
c ---[4685]---> BDD-cost:    1
c ---[4587]---> BDD-cost:    1
c ---[4489]---> BDD-cost:    1
c ---[4391]---> BDD-cost:    1
c ---[4350]---> BDD-cost:    1
c ---[4159]---> BDD-cost:    1
c ---[4061]---> BDD-cost:    1
c ---[3963]---> BDD-cost:    1
c ---[3865]---> BDD-cost:    1
c ---[3767]---> BDD-cost:    1
c ---[3726]---> BDD-cost:    1
c ---[3550]---> BDD-cost:    1
c ---[3377]---> BDD-cost:    1
c ---[3189]---> BDD-cost:    1
c ---[2986]---> BDD-cost:    1
c ---[2768]---> BDD-cost:    1
c ---[2399]---> BDD-cost:   17
c ---[2398]---> BDD-cost:    1
c ---[2397]---> BDD-cost:    1
c ---[2396]---> BDD-cost:   17
c ---[2395]---> BDD-cost:    1
c ---[2394]---> BDD-cost:    1
c ---[2393]---> BDD-cost:   17
c ---[2392]---> BDD-cost:    1
c ---[2391]---> BDD-cost:   14
c ---[2390]---> BDD-cost:   14
c ---[2389]---> BDD-cost:    1
c ---[2388]---> BDD-cost:    1
c ---[2387]---> BDD-cost:   17
c ---[2386]---> BDD-cost:    1
c ---[2385]---> BDD-cost:   14
c ---[2384]---> BDD-cost:   14
c ---[2383]---> BDD-cost:    1
c ---[2382]---> BDD-cost:    1
c ---[2381]---> BDD-cost:   17
c ---[2380]---> BDD-cost:    1
c ---[2379]---> BDD-cost:    1
c ---[2378]---> BDD-cost:   17
c ---[2377]---> BDD-cost:    1
c ---[2376]---> BDD-cost:    1
c ---[2375]---> BDD-cost:   17
c ---[2374]---> BDD-cost:    1
c ---[2373]---> BDD-cost:   24
c ---[2372]---> BDD-cost:    1
c ---[2371]---> BDD-cost:   21
c ---[2370]---> BDD-cost:    1
c ---[2369]---> BDD-cost:    1
c ---[2368]---> BDD-cost:    1
c ---[2367]---> BDD-cost:   14
c ---[2366]---> BDD-cost:   14
c ---[2365]---> BDD-cost:    1
c ---[2364]---> BDD-cost:    1
c ---[2363]---> BDD-cost:   14
c ---[2362]---> BDD-cost:   14
c ---[2361]---> BDD-cost:    1
c ---[2360]---> BDD-cost:    1
c ---[2359]---> BDD-cost:   14
c ---[2358]---> BDD-cost:   14
c ---[2357]---> BDD-cost:    1
c ---[2356]---> BDD-cost:    1
c ---[2355]---> BDD-cost:   14
c ---[2354]---> BDD-cost:   14
c ---[2353]---> BDD-cost:    1
c ---[2352]---> BDD-cost:    1
c ---[2351]---> BDD-cost:    1
c ---[2350]---> BDD-cost:    1
c ---[2349]---> BDD-cost:   21
c ---[2348]---> BDD-cost:    1
c ---[2347]---> BDD-cost:   24
c ---[2346]---> BDD-cost:    1
c ---[2345]---> BDD-cost:    1
c ---[2344]---> BDD-cost:    1
c ---[2343]---> BDD-cost:    1
c ---[2342]---> BDD-cost:    1
c ---[2341]---> BDD-cost:    1
c ---[2340]---> BDD-cost:   17
c ---[2339]---> BDD-cost:    1
c ---[2338]---> BDD-cost:    1
c ---[2337]---> BDD-cost:   17
c ---[2336]---> BDD-cost:    1
c ---[2335]---> BDD-cost:   21
c ---[2334]---> BDD-cost:    1
c ---[2333]---> BDD-cost:   21
c ---[2332]---> BDD-cost:    1
c ---[2331]---> BDD-cost:    1
c ---[2330]---> BDD-cost:    1
c ---[2329]---> BDD-cost:   14
c ---[2328]---> BDD-cost:   14
c ---[2327]---> BDD-cost:    1
c ---[2326]---> BDD-cost:    1
c ---[2325]---> BDD-cost:   14
c ---[2324]---> BDD-cost:   14
c ---[2323]---> BDD-cost:    1
c ---[2322]---> BDD-cost:    1
c ---[2321]---> BDD-cost:   14
c ---[2320]---> BDD-cost:   14
c ---[2319]---> BDD-cost:    1
c ---[2318]---> BDD-cost:    1
c ---[2317]---> BDD-cost:   14
c ---[2316]---> BDD-cost:   14
c ---[2315]---> BDD-cost:    1
c ---[2314]---> BDD-cost:    1
c ---[2313]---> BDD-cost:    1
c ---[2312]---> BDD-cost:    1
c ---[2311]---> BDD-cost:   21
c ---[2310]---> BDD-cost:    1
c ---[2309]---> BDD-cost:   21
c ---[2308]---> BDD-cost:    1
c ---[2307]---> BDD-cost:   24
c ---[2306]---> BDD-cost:    1
c ---[2305]---> BDD-cost:    1
c ---[2304]---> BDD-cost:    1
c ---[2303]---> BDD-cost:    1
c ---[2302]---> BDD-cost:    1
c ---[2301]---> BDD-cost:    1
c ---[2300]---> BDD-cost:    1
c ---[2299]---> BDD-cost:    1
c ---[2298]---> BDD-cost:    1
c ---[2297]---> BDD-cost:    1
c ---[2296]---> BDD-cost:   24
c ---[2295]---> BDD-cost:    1
c ---[2294]---> BDD-cost:    1
c ---[2293]---> BDD-cost:   17
c ---[2292]---> BDD-cost:    1
c ---[2291]---> BDD-cost:   19
c ---[2290]---> BDD-cost:    1
c ---[2289]---> BDD-cost:   16
c ---[2288]---> BDD-cost:    1
c ---[2287]---> BDD-cost:    1
c ---[2286]---> BDD-cost:    1
c ---[2285]---> BDD-cost:   14
c ---[2284]---> BDD-cost:   14
c ---[2283]---> BDD-cost:    1
c ---[2282]---> BDD-cost:    1
c ---[2281]---> BDD-cost:   14
c ---[2280]---> BDD-cost:   14
c ---[2279]---> BDD-cost:    1
c ---[2278]---> BDD-cost:    1
c ---[2277]---> BDD-cost:   14
c ---[2276]---> BDD-cost:   14
c ---[2275]---> BDD-cost:    1
c ---[2274]---> BDD-cost:    1
c ---[2273]---> BDD-cost:   14
c ---[2272]---> BDD-cost:   14
c ---[2271]---> BDD-cost:    1
c ---[2270]---> BDD-cost:    1
c ---[2269]---> BDD-cost:   14
c ---[2268]---> BDD-cost:   14
c ---[2267]---> BDD-cost:    1
c ---[2266]---> BDD-cost:    1
c ---[2265]---> BDD-cost:    1
c ---[2264]---> BDD-cost:    1
c ---[2263]---> BDD-cost:   16
c ---[2262]---> BDD-cost:    1
c ---[2261]---> BDD-cost:   19
c ---[2260]---> BDD-cost:    1
c ---[2259]---> BDD-cost:   19
c ---[2258]---> BDD-cost:    1
c ---[2257]---> BDD-cost:   22
c ---[2256]---> BDD-cost:    1
c ---[2255]---> BDD-cost:    1
c ---[2254]---> BDD-cost:    1
c ---[2253]---> BDD-cost:    1
c ---[2252]---> BDD-cost:    1
c ---[2251]---> BDD-cost:    1
c ---[2250]---> BDD-cost:    1
c ---[2249]---> BDD-cost:    1
c ---[2248]---> BDD-cost:    1
c ---[2247]---> BDD-cost:    1
c ---[2246]---> BDD-cost:    1
c ---[2245]---> BDD-cost:    1
c ---[2244]---> BDD-cost:    1
c ---[2243]---> BDD-cost:    1
c ---[2242]---> BDD-cost:   24
c ---[2241]---> BDD-cost:    1
c ---[2240]---> BDD-cost:    1
c ---[2239]---> BDD-cost:   17
c ---[2238]---> BDD-cost:    1
c ---[2237]---> BDD-cost:   16
c ---[2236]---> BDD-cost:    1
c ---[2235]---> BDD-cost:   16
c ---[2234]---> BDD-cost:    1
c ---[2233]---> BDD-cost:    1
c ---[2232]---> BDD-cost:    1
c ---[2231]---> BDD-cost:   14
c ---[2230]---> BDD-cost:   14
c ---[2229]---> BDD-cost:    1
c ---[2228]---> BDD-cost:    1
c ---[2227]---> BDD-cost:   14
c ---[2226]---> BDD-cost:   14
c ---[2225]---> BDD-cost:    1
c ---[2224]---> BDD-cost:    1
c ---[2223]---> BDD-cost:   14
c ---[2222]---> BDD-cost:   14
c ---[2221]---> BDD-cost:    1
c ---[2220]---> BDD-cost:    1
c ---[2219]---> BDD-cost:   14
c ---[2218]---> BDD-cost:   14
c ---[2217]---> BDD-cost:    1
c ---[2216]---> BDD-cost:    1
c ---[2215]---> BDD-cost:   14
c ---[2214]---> BDD-cost:   14
c ---[2213]---> BDD-cost:    1
c ---[2212]---> BDD-cost:    1
c ---[2211]---> BDD-cost:   14
c ---[2210]---> BDD-cost:   14
c ---[2209]---> BDD-cost:    1
c ---[2208]---> BDD-cost:    1
c ---[2207]---> BDD-cost:    1
c ---[2206]---> BDD-cost:    1
c ---[2205]---> BDD-cost:   16
c ---[2204]---> BDD-cost:    1
c ---[2203]---> BDD-cost:   16
c ---[2202]---> BDD-cost:    1
c ---[2201]---> BDD-cost:   19
c ---[2200]---> BDD-cost:    1
c ---[2199]---> BDD-cost:   19
c ---[2198]---> BDD-cost:    1
c ---[2197]---> BDD-cost:   22
c ---[2196]---> BDD-cost:    1
c ---[2195]---> BDD-cost:    1
c ---[2194]---> BDD-cost:    1
c ---[2193]---> BDD-cost:    1
c ---[2192]---> BDD-cost:    1
c ---[2191]---> BDD-cost:    1
c ---[2190]---> BDD-cost:    1
c ---[2189]---> BDD-cost:    1
c ---[2188]---> BDD-cost:    1
c ---[2187]---> BDD-cost:    1
c ---[2186]---> BDD-cost:    1
c ---[2185]---> BDD-cost:    1
c ---[2184]---> BDD-cost:    1
c ---[2183]---> BDD-cost:    1
c ---[2182]---> BDD-cost:    1
c ---[2181]---> BDD-cost:    1
c ---[2180]---> BDD-cost:    1
c ---[2179]---> BDD-cost:    1
c ---[2178]---> BDD-cost:   22
c ---[2177]---> BDD-cost:    1
c ---[2176]---> BDD-cost:    1
c ---[2175]---> BDD-cost:   17
c ---[2174]---> BDD-cost:    1
c ---[2173]---> BDD-cost:   16
c ---[2172]---> BDD-cost:    1
c ---[2171]---> BDD-cost:   16
c ---[2170]---> BDD-cost:    1
c ---[2169]---> BDD-cost:    1
c ---[2168]---> BDD-cost:    1
c ---[2167]---> BDD-cost:   14
c ---[2166]---> BDD-cost:   14
c ---[2165]---> BDD-cost:    1
c ---[2164]---> BDD-cost:    1
c ---[2163]---> BDD-cost:   14
c ---[2162]---> BDD-cost:   14
c ---[2161]---> BDD-cost:    1
c ---[2160]---> BDD-cost:    1
c ---[2159]---> BDD-cost:   14
c ---[2158]---> BDD-cost:   14
c ---[2157]---> BDD-cost:    1
c ---[2156]---> BDD-cost:    1
c ---[2155]---> BDD-cost:   14
c ---[2154]---> BDD-cost:   14
c ---[2153]---> BDD-cost:    1
c ---[2152]---> BDD-cost:    1
c ---[2151]---> BDD-cost:   14
c ---[2150]---> BDD-cost:   14
c ---[2149]---> BDD-cost:    1
c ---[2148]---> BDD-cost:    1
c ---[2147]---> BDD-cost:   14
c ---[2146]---> BDD-cost:   14
c ---[2145]---> BDD-cost:    1
c ---[2144]---> BDD-cost:    1
c ---[2143]---> BDD-cost:   14
c ---[2142]---> BDD-cost:   14
c ---[2141]---> BDD-cost:    1
c ---[2140]---> BDD-cost:    1
c ---[2139]---> BDD-cost:    1
c ---[2138]---> BDD-cost:    1
c ---[2137]---> BDD-cost:   16
c ---[2136]---> BDD-cost:    1
c ---[2135]---> BDD-cost:   16
c ---[2134]---> BDD-cost:    1
c ---[2133]---> BDD-cost:   16
c ---[2132]---> BDD-cost:    1
c ---[2131]---> BDD-cost:   21
c ---[2130]---> BDD-cost:    1
c ---[2129]---> BDD-cost:   21
c ---[2128]---> BDD-cost:    1
c ---[2127]---> BDD-cost:   24
c ---[2126]---> BDD-cost:    1
c ---[2125]---> BDD-cost:    1
c ---[2124]---> BDD-cost:    1
c ---[2123]---> BDD-cost:    1
c ---[2122]---> BDD-cost:    1
c ---[2121]---> BDD-cost:    1
c ---[2120]---> BDD-cost:    1
c ---[2119]---> BDD-cost:    1
c ---[2118]---> BDD-cost:    1
c ---[2117]---> BDD-cost:    1
c ---[2116]---> BDD-cost:    1
c ---[2115]---> BDD-cost:    1
c ---[2114]---> BDD-cost:    1
c ---[2113]---> BDD-cost:    1
c ---[2112]---> BDD-cost:    1
c ---[2111]---> BDD-cost:    1
c ---[2110]---> BDD-cost:    1
c ---[2109]---> BDD-cost:    1
c ---[2108]---> BDD-cost:    1
c ---[2107]---> BDD-cost:    1
c ---[2106]---> BDD-cost:    1
c ---[2105]---> BDD-cost:    1
c ---[2104]---> BDD-cost:   22
c ---[2103]---> BDD-cost:    1
c ---[2102]---> BDD-cost:    1
c ---[2101]---> BDD-cost:   17
c ---[2100]---> BDD-cost:    1
c ---[2099]---> BDD-cost:   11
c ---[2098]---> BDD-cost:    1
c ---[2097]---> BDD-cost:    1
c ---[2096]---> BDD-cost:    1
c ---[2095]---> BDD-cost:    1
c ---[2094]---> BDD-cost:    1
c ---[2093]---> BDD-cost:    1
c ---[2092]---> BDD-cost:   16
c ---[2091]---> BDD-cost:    1
c ---[2090]---> BDD-cost:    1
c ---[2089]---> BDD-cost:   17
c ---[2088]---> BDD-cost:    1
c ---[2087]---> BDD-cost:    1
c ---[2086]---> BDD-cost:   17
c ---[2085]---> BDD-cost:    1
c ---[2084]---> BDD-cost:    1
c ---[2083]---> BDD-cost:    1
c ---[2082]---> BDD-cost:    1
c ---[2081]---> BDD-cost:   17
c ---[2080]---> BDD-cost:    1
c ---[2079]---> BDD-cost:    1
c ---[2078]---> BDD-cost:   17
c ---[2077]---> BDD-cost:    1
c ---[2076]---> BDD-cost:    1
c ---[2075]---> BDD-cost:    1
c ---[2074]---> BDD-cost:    1
c ---[2073]---> BDD-cost:   17
c ---[2072]---> BDD-cost:   17
c ---[2071]---> BDD-cost:    1
c ---[2070]---> BDD-cost:    1
c ---[2069]---> BDD-cost:   17
c ---[2068]---> BDD-cost:    1
c ---[2067]---> BDD-cost:    1
c ---[2066]---> BDD-cost:   17
c ---[2065]---> BDD-cost:    1
c ---[2064]---> BDD-cost:    1
c ---[2063]---> BDD-cost:    1
c ---[2062]---> BDD-cost:    1
c ---[2061]---> BDD-cost:   17
c ---[2060]---> BDD-cost:   17
c ---[2059]---> BDD-cost:    1
c ---[2058]---> BDD-cost:    1
c ---[2057]---> BDD-cost:   17
c ---[2056]---> BDD-cost:   17
c ---[2055]---> BDD-cost:    1
c ---[2054]---> BDD-cost:    1
c ---[2053]---> BDD-cost:   17
c ---[2052]---> BDD-cost:    1
c ---[2051]---> BDD-cost:    1
c ---[2050]---> BDD-cost:   17
c ---[2049]---> BDD-cost:    1
c ---[2048]---> BDD-cost:    1
c ---[2047]---> BDD-cost:    1
c ---[2046]---> BDD-cost:    1
c ---[2045]---> BDD-cost:   17
c ---[2044]---> BDD-cost:   17
c ---[2043]---> BDD-cost:    1
c ---[2042]---> BDD-cost:    1
c ---[2041]---> BDD-cost:   17
c ---[2040]---> BDD-cost:   17
c ---[2039]---> BDD-cost:    1
c ---[2038]---> BDD-cost:    1
c ---[2037]---> BDD-cost:   17
c ---[2036]---> BDD-cost:   17
c ---[2035]---> BDD-cost:    1
c ---[2034]---> BDD-cost:    1
c ---[2033]---> BDD-cost:   17
c ---[2032]---> BDD-cost:    1
c ---[2031]---> BDD-cost:    1
c ---[2030]---> BDD-cost:   17
c ---[2029]---> BDD-cost:    1
c ---[2028]---> BDD-cost:    1
c ---[2027]---> BDD-cost:   21
c ---[2026]---> BDD-cost:    1
c ---[2025]---> BDD-cost:   17
c ---[2024]---> BDD-cost:   17
c ---[2023]---> BDD-cost:    1
c ---[2022]---> BDD-cost:    1
c ---[2021]---> BDD-cost:   17
c ---[2020]---> BDD-cost:   17
c ---[2019]---> BDD-cost:    1
c ---[2018]---> BDD-cost:    1
c ---[2017]---> BDD-cost:   17
c ---[2016]---> BDD-cost:   17
c ---[2015]---> BDD-cost:    1
c ---[2014]---> BDD-cost:    1
c ---[2013]---> BDD-cost:   17
c ---[2012]---> BDD-cost:   17
c ---[2011]---> BDD-cost:    1
c ---[2010]---> BDD-cost:    1
c ---[2009]---> BDD-cost:   17
c ---[2008]---> BDD-cost:    1
c ---[2007]---> BDD-cost:    1
c ---[2006]---> BDD-cost:   17
c ---[2005]---> BDD-cost:    1
c ---[2004]---> BDD-cost:    1
c ---[2003]---> BDD-cost:   21
c ---[2002]---> BDD-cost:    1
c ---[2001]---> BDD-cost:   17
c ---[2000]---> BDD-cost:   17
c ---[1999]---> BDD-cost:    1
c ---[1998]---> BDD-cost:    1
c ---[1997]---> BDD-cost:   17
c ---[1996]---> BDD-cost:   17
c ---[1995]---> BDD-cost:    1
c ---[1994]---> BDD-cost:    1
c ---[1993]---> BDD-cost:   17
c ---[1992]---> BDD-cost:   17
c ---[1991]---> BDD-cost:    1
c ---[1990]---> BDD-cost:    1
c ---[1989]---> BDD-cost:   17
c ---[1988]---> BDD-cost:   17
c ---[1987]---> BDD-cost:    1
c ---[1986]---> BDD-cost:    1
c ---[1985]---> BDD-cost:   17
c ---[1984]---> BDD-cost:   17
c ---[1983]---> BDD-cost:    1
c ---[1982]---> BDD-cost:    1
c ---[1981]---> BDD-cost:   17
c ---[1980]---> BDD-cost:    1
c ---[1979]---> BDD-cost:    1
c ---[1978]---> BDD-cost:   17
c ---[1977]---> BDD-cost:    1
c ---[1976]---> BDD-cost:    1
c ---[1975]---> BDD-cost:   21
c ---[1974]---> BDD-cost:    1
c ---[1973]---> BDD-cost:   17
c ---[1972]---> BDD-cost:   17
c ---[1971]---> BDD-cost:    1
c ---[1970]---> BDD-cost:    1
c ---[1969]---> BDD-cost:   17
c ---[1968]---> BDD-cost:   17
c ---[1967]---> BDD-cost:    1
c ---[1966]---> BDD-cost:    1
c ---[1965]---> BDD-cost:   17
c ---[1964]---> BDD-cost:   17
c ---[1963]---> BDD-cost:    1
c ---[1962]---> BDD-cost:    1
c ---[1961]---> BDD-cost:   17
c ---[1960]---> BDD-cost:   17
c ---[1959]---> BDD-cost:    1
c ---[1958]---> BDD-cost:    1
c ---[1957]---> BDD-cost:   17
c ---[1956]---> BDD-cost:   17
c ---[1955]---> BDD-cost:    1
c ---[1954]---> BDD-cost:    1
c ---[1953]---> BDD-cost:   17
c ---[1952]---> BDD-cost:   17
c ---[1951]---> BDD-cost:    1
c ---[1950]---> BDD-cost:    1
c ---[1949]---> BDD-cost:   17
c ---[1948]---> BDD-cost:    1
c ---[1947]---> BDD-cost:    1
c ---[1946]---> BDD-cost:   17
c ---[1945]---> BDD-cost:    1
c ---[1944]---> BDD-cost:    1
c ---[1943]---> BDD-cost:   21
c ---[1942]---> BDD-cost:    1
c ---[1941]---> BDD-cost:   17
c ---[1940]---> BDD-cost:   17
c ---[1939]---> BDD-cost:    1
c ---[1938]---> BDD-cost:    1
c ---[1937]---> BDD-cost:   17
c ---[1936]---> BDD-cost:   17
c ---[1935]---> BDD-cost:    1
c ---[1934]---> BDD-cost:    1
c ---[1933]---> BDD-cost:   17
c ---[1932]---> BDD-cost:   17
c ---[1931]---> BDD-cost:    1
c ---[1930]---> BDD-cost:    1
c ---[1929]---> BDD-cost:   17
c ---[1928]---> BDD-cost:   17
c ---[1927]---> BDD-cost:    1
c ---[1926]---> BDD-cost:    1
c ---[1925]---> BDD-cost:   17
c ---[1924]---> BDD-cost:   17
c ---[1923]---> BDD-cost:    1
c ---[1922]---> BDD-cost:    1
c ---[1921]---> BDD-cost:   17
c ---[1920]---> BDD-cost:   17
c ---[1919]---> BDD-cost:    1
c ---[1918]---> BDD-cost:    1
c ---[1917]---> BDD-cost:   17
c ---[1916]---> BDD-cost:   17
c ---[1915]---> BDD-cost:    1
c ---[1914]---> BDD-cost:    1
c ---[1913]---> BDD-cost:   17
c ---[1912]---> BDD-cost:    1
c ---[1911]---> BDD-cost:    1
c ---[1910]---> BDD-cost:   17
c ---[1909]---> BDD-cost:    1
c ---[1908]---> BDD-cost:    1
c ---[1907]---> BDD-cost:   16
c ---[1906]---> BDD-cost:    1
c ---[1905]---> BDD-cost:   17
c ---[1904]---> BDD-cost:   17
c ---[1903]---> BDD-cost:    1
c ---[1902]---> BDD-cost:    1
c ---[1901]---> BDD-cost:   17
c ---[1900]---> BDD-cost:   17
c ---[1899]---> BDD-cost:    1
c ---[1898]---> BDD-cost:    1
c ---[1897]---> BDD-cost:   17
c ---[1896]---> BDD-cost:   17
c ---[1895]---> BDD-cost:    1
c ---[1894]---> BDD-cost:    1
c ---[1893]---> BDD-cost:   17
c ---[1892]---> BDD-cost:   17
c ---[1891]---> BDD-cost:    1
c ---[1890]---> BDD-cost:    1
c ---[1889]---> BDD-cost:   17
c ---[1888]---> BDD-cost:   17
c ---[1887]---> BDD-cost:    1
c ---[1886]---> BDD-cost:    1
c ---[1885]---> BDD-cost:   17
c ---[1884]---> BDD-cost:   17
c ---[1883]---> BDD-cost:    1
c ---[1882]---> BDD-cost:    1
c ---[1881]---> BDD-cost:   17
c ---[1880]---> BDD-cost:   17
c ---[1879]---> BDD-cost:    1
c ---[1878]---> BDD-cost:    1
c ---[1877]---> BDD-cost:   17
c ---[1876]---> BDD-cost:   17
c ---[1875]---> BDD-cost:    1
c ---[1874]---> BDD-cost:    1
c ---[1873]---> BDD-cost:   17
c ---[1872]---> BDD-cost:    1
c ---[1871]---> BDD-cost:    1
c ---[1870]---> BDD-cost:   17
c ---[1869]---> BDD-cost:    1
c ---[1868]---> BDD-cost:    1
c ---[1867]---> BDD-cost:   16
c ---[1866]---> BDD-cost:    1
c ---[1865]---> BDD-cost:   17
c ---[1864]---> BDD-cost:   17
c ---[1863]---> BDD-cost:    1
c ---[1862]---> BDD-cost:    1
c ---[1861]---> BDD-cost:   17
c ---[1860]---> BDD-cost:   17
c ---[1859]---> BDD-cost:    1
c ---[1858]---> BDD-cost:    1
c ---[1857]---> BDD-cost:   17
c ---[1856]---> BDD-cost:   17
c ---[1855]---> BDD-cost:    1
c ---[1854]---> BDD-cost:    1
c ---[1853]---> BDD-cost:   17
c ---[1852]---> BDD-cost:   17
c ---[1851]---> BDD-cost:    1
c ---[1850]---> BDD-cost:    1
c ---[1849]---> BDD-cost:   17
c ---[1848]---> BDD-cost:   17
c ---[1847]---> BDD-cost:    1
c ---[1846]---> BDD-cost:    1
c ---[1845]---> BDD-cost:   17
c ---[1844]---> BDD-cost:   17
c ---[1843]---> BDD-cost:    1
c ---[1842]---> BDD-cost:    1
c ---[1841]---> BDD-cost:   17
c ---[1840]---> BDD-cost:   17
c ---[1839]---> BDD-cost:    1
c ---[1838]---> BDD-cost:    1
c ---[1837]---> BDD-cost:   17
c ---[1836]---> BDD-cost:   17
c ---[1835]---> BDD-cost:    1
c ---[1834]---> BDD-cost:    1
c ---[1833]---> BDD-cost:   17
c ---[1832]---> BDD-cost:   17
c ---[1831]---> BDD-cost:    1
c ---[1830]---> BDD-cost:    1
c ---[1829]---> BDD-cost:   17
c ---[1828]---> BDD-cost:    1
c ---[1827]---> BDD-cost:    1
c ---[1826]---> BDD-cost:   17
c ---[1825]---> BDD-cost:    1
c ---[1824]---> BDD-cost:    1
c ---[1823]---> BDD-cost:   16
c ---[1822]---> BDD-cost:    1
c ---[1821]---> BDD-cost:   17
c ---[1820]---> BDD-cost:   17
c ---[1819]---> BDD-cost:    1
c ---[1818]---> BDD-cost:    1
c ---[1817]---> BDD-cost:   17
c ---[1816]---> BDD-cost:   17
c ---[1815]---> BDD-cost:    1
c ---[1814]---> BDD-cost:    1
c ---[1813]---> BDD-cost:   17
c ---[1812]---> BDD-cost:   17
c ---[1811]---> BDD-cost:    1
c ---[1810]---> BDD-cost:    1
c ---[1809]---> BDD-cost:   17
c ---[1808]---> BDD-cost:   17
c ---[1807]---> BDD-cost:    1
c ---[1806]---> BDD-cost:    1
c ---[1805]---> BDD-cost:   17
c ---[1804]---> BDD-cost:   17
c ---[1803]---> BDD-cost:    1
c ---[1802]---> BDD-cost:    1
c ---[1801]---> BDD-cost:   17
c ---[1800]---> BDD-cost:   17
c ---[1799]---> BDD-cost:    1
c ---[1798]---> BDD-cost:    1
c ---[1797]---> BDD-cost:   17
c ---[1796]---> BDD-cost:   17
c ---[1795]---> BDD-cost:    1
c ---[1794]---> BDD-cost:    1
c ---[1793]---> BDD-cost:   17
c ---[1792]---> BDD-cost:   17
c ---[1791]---> BDD-cost:    1
c ---[1790]---> BDD-cost:    1
c ---[1789]---> BDD-cost:   17
c ---[1788]---> BDD-cost:   17
c ---[1787]---> BDD-cost:    1
c ---[1786]---> BDD-cost:    1
c ---[1785]---> BDD-cost:   17
c ---[1784]---> BDD-cost:   17
c ---[1783]---> BDD-cost:    1
c ---[1782]---> BDD-cost:    1
c ---[1781]---> BDD-cost:   17
c ---[1780]---> BDD-cost:    1
c ---[1779]---> BDD-cost:    1
c ---[1778]---> BDD-cost:   17
c ---[1777]---> BDD-cost:    1
c ---[1776]---> BDD-cost:    1
c ---[1775]---> BDD-cost:   16
c ---[1774]---> BDD-cost:    1
c ---[1773]---> BDD-cost:   17
c ---[1772]---> BDD-cost:   17
c ---[1771]---> BDD-cost:    1
c ---[1770]---> BDD-cost:    1
c ---[1769]---> BDD-cost:   17
c ---[1768]---> BDD-cost:   17
c ---[1767]---> BDD-cost:    1
c ---[1766]---> BDD-cost:    1
c ---[1765]---> BDD-cost:   17
c ---[1764]---> BDD-cost:   17
c ---[1763]---> BDD-cost:    1
c ---[1762]---> BDD-cost:    1
c ---[1761]---> BDD-cost:   17
c ---[1760]---> BDD-cost:   17
c ---[1759]---> BDD-cost:    1
c ---[1758]---> BDD-cost:    1
c ---[1757]---> BDD-cost:   17
c ---[1756]---> BDD-cost:   17
c ---[1755]---> BDD-cost:    1
c ---[1754]---> BDD-cost:    1
c ---[1753]---> BDD-cost:   17
c ---[1752]---> BDD-cost:   17
c ---[1751]---> BDD-cost:    1
c ---[1750]---> BDD-cost:    1
c ---[1749]---> BDD-cost:   17
c ---[1748]---> BDD-cost:   17
c ---[1747]---> BDD-cost:    1
c ---[1746]---> BDD-cost:    1
c ---[1745]---> BDD-cost:   17
c ---[1744]---> BDD-cost:   17
c ---[1743]---> BDD-cost:    1
c ---[1742]---> BDD-cost:    1
c ---[1741]---> BDD-cost:   17
c ---[1740]---> BDD-cost:   17
c ---[1739]---> BDD-cost:    1
c ---[1738]---> BDD-cost:    1
c ---[1737]---> BDD-cost:   17
c ---[1736]---> BDD-cost:   17
c ---[1735]---> BDD-cost:    1
c ---[1734]---> BDD-cost:    1
c ---[1733]---> BDD-cost:   17
c ---[1732]---> BDD-cost:   17
c ---[1731]---> BDD-cost:    1
c ---[1730]---> BDD-cost:    1
c ---[1729]---> BDD-cost:   14
c ---[1728]---> BDD-cost:   14
c ---[1727]---> BDD-cost:    1
c ---[1726]---> BDD-cost:    1
c ---[1725]---> BDD-cost:   14
c ---[1724]---> BDD-cost:   14
c ---[1723]---> BDD-cost:    1
c ---[1722]---> BDD-cost:    1
c ---[1721]---> BDD-cost:   14
c ---[1720]---> BDD-cost:   14
c ---[1719]---> BDD-cost:    1
c ---[1718]---> BDD-cost:    1
c ---[1717]---> BDD-cost:   14
c ---[1716]---> BDD-cost:   14
c ---[1715]---> BDD-cost:    1
c ---[1714]---> BDD-cost:    1
c ---[1713]---> BDD-cost:   14
c ---[1712]---> BDD-cost:   14
c ---[1711]---> BDD-cost:    1
c ---[1710]---> BDD-cost:    1
c ---[1709]---> BDD-cost:   14
c ---[1708]---> BDD-cost:   14
c ---[1707]---> BDD-cost:    1
c ---[1706]---> BDD-cost:    1
c ---[1705]---> BDD-cost:   14
c ---[1704]---> BDD-cost:   14
c ---[1703]---> BDD-cost:    1
c ---[1702]---> BDD-cost:    1
c ---[1701]---> BDD-cost:   14
c ---[1700]---> BDD-cost:   14
c ---[1699]---> BDD-cost:    1
c ---[1698]---> BDD-cost:    1
c ---[1697]---> BDD-cost:    1
c ---[1696]---> BDD-cost:    1
c ---[1695]---> BDD-cost:   11
c ---[1694]---> BDD-cost:    1
c ---[1693]---> BDD-cost:   11
c ---[1692]---> BDD-cost:    1
c ---[1691]---> BDD-cost:   11
c ---[1690]---> BDD-cost:    1
c ---[1689]---> BDD-cost:   11
c ---[1688]---> BDD-cost:    1
c ---[1687]---> BDD-cost:   17
c ---[1686]---> BDD-cost:    1
c ---[1685]---> BDD-cost:    1
c ---[1684]---> BDD-cost:   11
c ---[1683]---> BDD-cost:    1
c ---[1682]---> BDD-cost:    1
c ---[1681]---> BDD-cost:    1
c ---[1680]---> BDD-cost:   11
c ---[1679]---> BDD-cost:    1
c ---[1678]---> BDD-cost:    1
c ---[1677]---> BDD-cost:    1
c ---[1676]---> BDD-cost:   11
c ---[1675]---> BDD-cost:    1
c ---[1674]---> BDD-cost:    1
c ---[1673]---> BDD-cost:    1
c ---[1672]---> BDD-cost:   11
c ---[1671]---> BDD-cost:    1
c ---[1670]---> BDD-cost:    1
c ---[1669]---> BDD-cost:    1
c ---[1668]---> BDD-cost:   14
c ---[1667]---> BDD-cost:    1
c ---[1666]---> BDD-cost:    1
c ---[1665]---> BDD-cost:    1
c ---[1664]---> BDD-cost:   17
c ---[1663]---> BDD-cost:    1
c ---[1662]---> BDD-cost:    1
c ---[1661]---> BDD-cost:   17
c ---[1660]---> BDD-cost:    1
c ---[1659]---> BDD-cost:   17
c ---[1658]---> BDD-cost:   17
c ---[1657]---> BDD-cost:    1
c ---[1656]---> BDD-cost:    1
c ---[1655]---> BDD-cost:   17
c ---[1654]---> BDD-cost:   17
c ---[1653]---> BDD-cost:    1
c ---[1652]---> BDD-cost:    1
c ---[1651]---> BDD-cost:   17
c ---[1650]---> BDD-cost:   17
c ---[1649]---> BDD-cost:    1
c ---[1648]---> BDD-cost:    1
c ---[1647]---> BDD-cost:   17
c ---[1646]---> BDD-cost:   17
c ---[1645]---> BDD-cost:    1
c ---[1644]---> BDD-cost:    1
c ---[1643]---> BDD-cost:   17
c ---[1642]---> BDD-cost:   17
c ---[1641]---> BDD-cost:    1
c ---[1640]---> BDD-cost:    1
c ---[1639]---> BDD-cost:   17
c ---[1638]---> BDD-cost:   17
c ---[1637]---> BDD-cost:    1
c ---[1636]---> BDD-cost:    1
c ---[1635]---> BDD-cost:   17
c ---[1634]---> BDD-cost:   17
c ---[1633]---> BDD-cost:    1
c ---[1632]---> BDD-cost:    1
c ---[1631]---> BDD-cost:    1
c ---[1630]---> BDD-cost:    1
c ---[1629]---> BDD-cost:    1
c ---[1628]---> BDD-cost:    1
c ---[1627]---> BDD-cost:   16
c ---[1626]---> BDD-cost:    1
c ---[1625]---> BDD-cost:    1
c ---[1624]---> BDD-cost:    1
c ---[1623]---> BDD-cost:   16
c ---[1622]---> BDD-cost:    1
c ---[1621]---> BDD-cost:    1
c ---[1620]---> BDD-cost:    1
c ---[1619]---> BDD-cost:   16
c ---[1618]---> BDD-cost:    1
c ---[1617]---> BDD-cost:    1
c ---[1616]---> BDD-cost:    1
c ---[1615]---> BDD-cost:   21
c ---[1614]---> BDD-cost:    1
c ---[1613]---> BDD-cost:    1
c ---[1612]---> BDD-cost:    1
c ---[1611]---> BDD-cost:    1
c ---[1610]---> BDD-cost:    1
c ---[1609]---> BDD-cost:    1
c ---[1608]---> BDD-cost:    1
c ---[1607]---> BDD-cost:   21
c ---[1606]---> BDD-cost:    1
c ---[1605]---> BDD-cost:    1
c ---[1604]---> BDD-cost:    1
c ---[1603]---> BDD-cost:   21
c ---[1602]---> BDD-cost:    1
c ---[1601]---> BDD-cost:    1
c ---[1600]---> BDD-cost:    1
c ---[1599]---> BDD-cost:   21
c ---[1598]---> BDD-cost:    1
c ---[1597]---> BDD-cost:    1
c ---[1596]---> BDD-cost:    1
c ---[1595]---> BDD-cost:    1
c ---[1594]---> BDD-cost:    1
c ---[1593]---> BDD-cost:    1
c ---[1592]---> BDD-cost:    1
c ---[1591]---> BDD-cost:   16
c ---[1590]---> BDD-cost:    1
c ---[1589]---> BDD-cost:    1
c ---[1588]---> BDD-cost:    1
c ---[1587]---> BDD-cost:   16
c ---[1586]---> BDD-cost:    1
c ---[1585]---> BDD-cost:    1
c ---[1584]---> BDD-cost:    1
c ---[1583]---> BDD-cost:    1
c ---[1582]---> BDD-cost:    1
c ---[1581]---> BDD-cost:    1
c ---[1580]---> BDD-cost:    1
c ---[1579]---> BDD-cost:   16
c ---[1578]---> BDD-cost:    1
c ---[1577]---> BDD-cost:    1
c ---[1576]---> BDD-cost:    1
c ---[1575]---> BDD-cost:   16
c ---[1574]---> BDD-cost:    1
c ---[1573]---> BDD-cost:    1
c ---[1572]---> BDD-cost:    1
c ---[1571]---> BDD-cost:   14
c ---[1570]---> BDD-cost:   14
c ---[1569]---> BDD-cost:    1
c ---[1568]---> BDD-cost:    1
c ---[1567]---> BDD-cost:    1
c ---[1566]---> BDD-cost:    1
c ---[1565]---> BDD-cost:    0
c ---[1564]---> BDD-cost:    0
c ---[1563]---> BDD-cost:    1
c ---[1562]---> BDD-cost:    1
c ---[1561]---> BDD-cost:    0
c ---[1560]---> BDD-cost:    0
c ---[1559]---> BDD-cost:    0
c ---[1558]---> BDD-cost:    0
c ---[1557]---> BDD-cost:    0
c ---[1556]---> BDD-cost:    0
c ---[1555]---> BDD-cost:    0
c ---[1554]---> BDD-cost:    0
c ---[1553]---> BDD-cost:    1
c ---[1552]---> BDD-cost:    1
c ---[1551]---> BDD-cost:    1
c ---[1550]---> BDD-cost:    1
c ---[1549]---> BDD-cost:    1
c ---[1548]---> BDD-cost:    1
c ---[1547]---> BDD-cost:    1
c ---[1546]---> BDD-cost:    1
c ---[1545]---> BDD-cost:    1
c ---[1544]---> BDD-cost:    1
c ---[1543]---> BDD-cost:    1
c ---[1542]---> BDD-cost:    1
c ---[1541]---> BDD-cost:    1
c ---[1540]---> BDD-cost:    1
c ---[1539]---> BDD-cost:    1
c ---[1538]---> BDD-cost:    1
c ---[1537]---> BDD-cost:    1
c ---[1536]---> BDD-cost:    1
c ---[1535]---> BDD-cost:    1
c ---[1534]---> BDD-cost:    1
c ---[1533]---> BDD-cost:   14
c ---[1532]---> BDD-cost:   14
c ---[1531]---> BDD-cost:    1
c ---[1530]---> BDD-cost:    1
c ---[1529]---> BDD-cost:   16
c ---[1528]---> BDD-cost:    1
c ---[1527]---> BDD-cost:    1
c ---[1526]---> BDD-cost:    1
c ---[1525]---> BDD-cost:   14
c ---[1524]---> BDD-cost:   14
c ---[1523]---> BDD-cost:    1
c ---[1522]---> BDD-cost:    1
c ---[1521]---> BDD-cost:   14
c ---[1520]---> BDD-cost:   14
c ---[1519]---> BDD-cost:    1
c ---[1518]---> BDD-cost:    1
c ---[1517]---> BDD-cost:   14
c ---[1516]---> BDD-cost:   14
c ---[1515]---> BDD-cost:    1
c ---[1514]---> BDD-cost:    1
c ---[1513]---> BDD-cost:   14
c ---[1512]---> BDD-cost:   14
c ---[1511]---> BDD-cost:    1
c ---[1510]---> BDD-cost:    1
c ---[1509]---> BDD-cost:   14
c ---[1508]---> BDD-cost:   14
c ---[1507]---> BDD-cost:    1
c ---[1506]---> BDD-cost:    1
c ---[1505]---> BDD-cost:   14
c ---[1504]---> BDD-cost:   14
c ---[1503]---> BDD-cost:    1
c ---[1502]---> BDD-cost:    1
c ---[1501]---> BDD-cost:   14
c ---[1500]---> BDD-cost:   14
c ---[1499]---> BDD-cost:    1
c ---[1498]---> BDD-cost:    1
c ---[1497]---> BDD-cost:   16
c ---[1496]---> BDD-cost:    1
c ---[1495]---> BDD-cost:    1
c ---[1494]---> BDD-cost:    1
c ---[1493]---> BDD-cost:   16
c ---[1492]---> BDD-cost:    1
c ---[1491]---> BDD-cost:    1
c ---[1490]---> BDD-cost:    1
c ---[1489]---> BDD-cost:   16
c ---[1488]---> BDD-cost:    1
c ---[1487]---> BDD-cost:    1
c ---[1486]---> BDD-cost:    1
c ---[1485]---> BDD-cost:   16
c ---[1484]---> BDD-cost:    1
c ---[1483]---> BDD-cost:    1
c ---[1482]---> BDD-cost:    1
c ---[1481]---> BDD-cost:   16
c ---[1480]---> BDD-cost:    1
c ---[1479]---> BDD-cost:    1
c ---[1478]---> BDD-cost:    1
c ---[1477]---> BDD-cost:   16
c ---[1476]---> BDD-cost:    1
c ---[1475]---> BDD-cost:    1
c ---[1474]---> BDD-cost:    1
c ---[1473]---> BDD-cost:   16
c ---[1472]---> BDD-cost:    1
c ---[1471]---> BDD-cost:    1
c ---[1470]---> BDD-cost:    1
c ---[1469]---> BDD-cost:   14
c ---[1468]---> BDD-cost:   14
c ---[1467]---> BDD-cost:    1
c ---[1466]---> BDD-cost:    1
c ---[1465]---> BDD-cost:   14
c ---[1464]---> BDD-cost:   14
c ---[1463]---> BDD-cost:    1
c ---[1462]---> BDD-cost:    1
c ---[1461]---> BDD-cost:    0
c ---[1460]---> BDD-cost:    0
c ---[1459]---> BDD-cost:   17
c ---[1458]---> BDD-cost:   17
c ---[1457]---> BDD-cost:    1
c ---[1456]---> BDD-cost:    1
c ---[1455]---> BDD-cost:   17
c ---[1454]---> BDD-cost:   17
c ---[1453]---> BDD-cost:    1
c ---[1452]---> BDD-cost:    1
c ---[1451]---> BDD-cost:   17
c ---[1450]---> BDD-cost:   17
c ---[1449]---> BDD-cost:    1
c ---[1448]---> BDD-cost:    1
c ---[1447]---> BDD-cost:   17
c ---[1446]---> BDD-cost:   17
c ---[1445]---> BDD-cost:    1
c ---[1444]---> BDD-cost:    1
c ---[1443]---> BDD-cost:   17
c ---[1442]---> BDD-cost:   17
c ---[1441]---> BDD-cost:    1
c ---[1440]---> BDD-cost:    1
c ---[1439]---> BDD-cost:   17
c ---[1438]---> BDD-cost:   17
c ---[1437]---> BDD-cost:    1
c ---[1436]---> BDD-cost:    1
c ---[1435]---> BDD-cost:   17
c ---[1434]---> BDD-cost:   17
c ---[1433]---> BDD-cost:    1
c ---[1432]---> BDD-cost:    1
c ---[1431]---> BDD-cost:   17
c ---[1430]---> BDD-cost:   17
c ---[1429]---> BDD-cost:    1
c ---[1428]---> BDD-cost:    1
c ---[1427]---> BDD-cost:   17
c ---[1426]---> BDD-cost:   17
c ---[1425]---> BDD-cost:    1
c ---[1424]---> BDD-cost:    1
c ---[1423]---> BDD-cost:   17
c ---[1422]---> BDD-cost:   17
c ---[1421]---> BDD-cost:    1
c ---[1420]---> BDD-cost:    1
c ---[1419]---> BDD-cost:   17
c ---[1418]---> BDD-cost:   17
c ---[1417]---> BDD-cost:    1
c ---[1416]---> BDD-cost:    1
c ---[1415]---> BDD-cost:   17
c ---[1414]---> BDD-cost:   17
c ---[1413]---> BDD-cost:    1
c ---[1412]---> BDD-cost:    1
c ---[1411]---> BDD-cost:   17
c ---[1410]---> BDD-cost:    1
c ---[1409]---> BDD-cost:    1
c ---[1408]---> BDD-cost:   17
c ---[1407]---> BDD-cost:    1
c ---[1406]---> BDD-cost:    1
c ---[1405]---> BDD-cost:   17
c ---[1404]---> BDD-cost:    1
c ---[1403]---> BDD-cost:    1
c ---[1402]---> BDD-cost:   21
c ---[1401]---> BDD-cost:    1
c ---[1400]---> BDD-cost:    1
c ---[1399]---> BDD-cost:    1
c ---[1398]---> BDD-cost:   21
c ---[1397]---> BDD-cost:    1
c ---[1396]---> BDD-cost:    1
c ---[1395]---> BDD-cost:    1
c ---[1394]---> BDD-cost:   16
c ---[1393]---> BDD-cost:    1
c ---[1392]---> BDD-cost:    1
c ---[1391]---> BDD-cost:    1
c ---[1390]---> BDD-cost:   16
c ---[1389]---> BDD-cost:    1
c ---[1388]---> BDD-cost:    1
c ---[1387]---> BDD-cost:    1
c ---[1386]---> BDD-cost:   16
c ---[1385]---> BDD-cost:    1
c ---[1384]---> BDD-cost:    1
c ---[1383]---> BDD-cost:   17
c ---[1382]---> BDD-cost:   17
c ---[1381]---> BDD-cost:    1
c ---[1380]---> BDD-cost:    1
c ---[1379]---> BDD-cost:   17
c ---[1378]---> BDD-cost:   17
c ---[1377]---> BDD-cost:    1
c ---[1376]---> BDD-cost:    1
c ---[1375]---> BDD-cost:   17
c ---[1374]---> BDD-cost:   17
c ---[1373]---> BDD-cost:    1
c ---[1372]---> BDD-cost:    1
c ---[1371]---> BDD-cost:   17
c ---[1370]---> BDD-cost:   17
c ---[1369]---> BDD-cost:    1
c ---[1368]---> BDD-cost:    1
c ---[1367]---> BDD-cost:   17
c ---[1366]---> BDD-cost:   17
c ---[1365]---> BDD-cost:    1
c ---[1364]---> BDD-cost:    1
c ---[1363]---> BDD-cost:   17
c ---[1362]---> BDD-cost:   17
c ---[1361]---> BDD-cost:    1
c ---[1360]---> BDD-cost:    1
c ---[1359]---> BDD-cost:   17
c ---[1358]---> BDD-cost:   17
c ---[1357]---> BDD-cost:    1
c ---[1356]---> BDD-cost:    1
c ---[1355]---> BDD-cost:   17
c ---[1354]---> BDD-cost:   17
c ---[1353]---> BDD-cost:    1
c ---[1352]---> BDD-cost:    1
c ---[1351]---> BDD-cost:   17
c ---[1350]---> BDD-cost:   17
c ---[1349]---> BDD-cost:    1
c ---[1348]---> BDD-cost:    1
c ---[1347]---> BDD-cost:   17
c ---[1346]---> BDD-cost:   17
c ---[1345]---> BDD-cost:    1
c ---[1344]---> BDD-cost:    1
c ---[1343]---> BDD-cost:   17
c ---[1342]---> BDD-cost:   17
c ---[1341]---> BDD-cost:    1
c ---[1340]---> BDD-cost:    1
c ---[1339]---> BDD-cost:   17
c ---[1338]---> BDD-cost:   17
c ---[1337]---> BDD-cost:    1
c ---[1336]---> BDD-cost:    1
c ---[1335]---> BDD-cost:   17
c ---[1334]---> BDD-cost:   17
c ---[1333]---> BDD-cost:    1
c ---[1332]---> BDD-cost:    1
c ---[1331]---> BDD-cost:   17
c ---[1330]---> BDD-cost:   17
c ---[1329]---> BDD-cost:    1
c ---[1328]---> BDD-cost:    1
c ---[1327]---> BDD-cost:   17
c ---[1326]---> BDD-cost:   17
c ---[1325]---> BDD-cost:    1
c ---[1324]---> BDD-cost:    1
c ---[1323]---> BDD-cost:   17
c ---[1322]---> BDD-cost:   17
c ---[1321]---> BDD-cost:    1
c ---[1320]---> BDD-cost:    1
c ---[1319]---> BDD-cost:   17
c ---[1318]---> BDD-cost:   17
c ---[1317]---> BDD-cost:    1
c ---[1316]---> BDD-cost:    1
c ---[1315]---> BDD-cost:   17
c ---[1314]---> BDD-cost:   17
c ---[1313]---> BDD-cost:    1
c ---[1312]---> BDD-cost:    1
c ---[1311]---> BDD-cost:   17
c ---[1310]---> BDD-cost:   17
c ---[1309]---> BDD-cost:    1
c ---[1308]---> BDD-cost:    1
c ---[1307]---> BDD-cost:   17
c ---[1306]---> BDD-cost:   17
c ---[1305]---> BDD-cost:    1
c ---[1304]---> BDD-cost:    1
c ---[1303]---> BDD-cost:   17
c ---[1302]---> BDD-cost:   17
c ---[1301]---> BDD-cost:    1
c ---[1300]---> BDD-cost:    1
c ---[1299]---> BDD-cost:   17
c ---[1298]---> BDD-cost:   17
c ---[1297]---> BDD-cost:    1
c ---[1296]---> BDD-cost:    1
c ---[1295]---> BDD-cost:   17
c ---[1294]---> BDD-cost:   17
c ---[1293]---> BDD-cost:    1
c ---[1292]---> BDD-cost:    1
c ---[1291]---> BDD-cost:   17
c ---[1290]---> BDD-cost:   17
c ---[1289]---> BDD-cost:    1
c ---[1288]---> BDD-cost:    1
c ---[1287]---> BDD-cost:   17
c ---[1286]---> BDD-cost:   17
c ---[1285]---> BDD-cost:    1
c ---[1284]---> BDD-cost:    1
c ---[1283]---> BDD-cost:   17
c ---[1282]---> BDD-cost:   17
c ---[1281]---> BDD-cost:    1
c ---[1280]---> BDD-cost:    1
c ---[1279]---> BDD-cost:   17
c ---[1278]---> BDD-cost:   17
c ---[1277]---> BDD-cost:    1
c ---[1276]---> BDD-cost:    1
c ---[1275]---> BDD-cost:   17
c ---[1274]---> BDD-cost:   17
c ---[1273]---> BDD-cost:    1
c ---[1272]---> BDD-cost:    1
c ---[1271]---> BDD-cost:   17
c ---[1270]---> BDD-cost:   17
c ---[1269]---> BDD-cost:    1
c ---[1268]---> BDD-cost:    1
c ---[1267]---> BDD-cost:   17
c ---[1266]---> BDD-cost:   17
c ---[1265]---> BDD-cost:    1
c ---[1264]---> BDD-cost:    1
c ---[1263]---> BDD-cost:   17
c ---[1262]---> BDD-cost:   17
c ---[1261]---> BDD-cost:    1
c ---[1260]---> BDD-cost:    1
c ---[1259]---> BDD-cost:   17
c ---[1258]---> BDD-cost:   17
c ---[1257]---> BDD-cost:    1
c ---[1256]---> BDD-cost:    1
c ---[1255]---> BDD-cost:   17
c ---[1254]---> BDD-cost:   17
c ---[1253]---> BDD-cost:    1
c ---[1252]---> BDD-cost:    1
c ---[1251]---> BDD-cost:   17
c ---[1250]---> BDD-cost:   17
c ---[1249]---> BDD-cost:    1
c ---[1248]---> BDD-cost:    1
c ---[1247]---> BDD-cost:   17
c ---[1246]---> BDD-cost:   17
c ---[1245]---> BDD-cost:    1
c ---[1244]---> BDD-cost:    1
c ---[1243]---> BDD-cost:   17
c ---[1242]---> BDD-cost:   17
c ---[1241]---> BDD-cost:    1
c ---[1240]---> BDD-cost:    1
c ---[1239]---> BDD-cost:   17
c ---[1238]---> BDD-cost:   17
c ---[1237]---> BDD-cost:    1
c ---[1236]---> BDD-cost:    1
c ---[1235]---> BDD-cost:   17
c ---[1234]---> BDD-cost:   17
c ---[1233]---> BDD-cost:    1
c ---[1232]---> BDD-cost:    1
c ---[1231]---> BDD-cost:   17
c ---[1230]---> BDD-cost:   17
c ---[1229]---> BDD-cost:    1
c ---[1228]---> BDD-cost:    1
c ---[1227]---> BDD-cost:   17
c ---[1226]---> BDD-cost:   17
c ---[1225]---> BDD-cost:    1
c ---[1224]---> BDD-cost:    1
c ---[1223]---> BDD-cost:   17
c ---[1222]---> BDD-cost:   17
c ---[1221]---> BDD-cost:    1
c ---[1220]---> BDD-cost:    1
c ---[1219]---> BDD-cost:   17
c ---[1218]---> BDD-cost:   17
c ---[1217]---> BDD-cost:    1
c ---[1216]---> BDD-cost:    1
c ---[1215]---> BDD-cost:   17
c ---[1214]---> BDD-cost:   17
c ---[1213]---> BDD-cost:    1
c ---[1212]---> BDD-cost:    1
c ---[1211]---> BDD-cost:   17
c ---[1210]---> BDD-cost:   17
c ---[1209]---> BDD-cost:    1
c ---[1208]---> BDD-cost:    1
c ---[1207]---> BDD-cost:   17
c ---[1206]---> BDD-cost:   17
c ---[1205]---> BDD-cost:    1
c ---[1204]---> BDD-cost:    1
c ---[1203]---> BDD-cost:   17
c ---[1202]---> BDD-cost:   17
c ---[1201]---> BDD-cost:    1
c ---[1200]---> BDD-cost:    1
c ---[1199]---> BDD-cost:   17
c ---[1198]---> BDD-cost:   17
c ---[1197]---> BDD-cost:    1
c ---[1196]---> BDD-cost:    1
c ---[1195]---> BDD-cost:   17
c ---[1194]---> BDD-cost:   17
c ---[1193]---> BDD-cost:    1
c ---[1192]---> BDD-cost:    1
c ---[1191]---> BDD-cost:   17
c ---[1190]---> BDD-cost:   17
c ---[1189]---> BDD-cost:    1
c ---[1188]---> BDD-cost:    1
c ---[1187]---> BDD-cost:   17
c ---[1186]---> BDD-cost:   17
c ---[1185]---> BDD-cost:    1
c ---[1184]---> BDD-cost:    1
c ---[1183]---> BDD-cost:   17
c ---[1182]---> BDD-cost:   17
c ---[1181]---> BDD-cost:    1
c ---[1180]---> BDD-cost:    1
c ---[1179]---> BDD-cost:   17
c ---[1178]---> BDD-cost:   17
c ---[1177]---> BDD-cost:    1
c ---[1176]---> BDD-cost:    1
c ---[1175]---> BDD-cost:   17
c ---[1174]---> BDD-cost:   17
c ---[1173]---> BDD-cost:    1
c ---[1172]---> BDD-cost:    1
c ---[1171]---> BDD-cost:   17
c ---[1170]---> BDD-cost:   17
c ---[1169]---> BDD-cost:    1
c ---[1168]---> BDD-cost:    1
c ---[1167]---> BDD-cost:   17
c ---[1166]---> BDD-cost:   17
c ---[1165]---> BDD-cost:    1
c ---[1164]---> BDD-cost:    1
c ---[1163]---> BDD-cost:   17
c ---[1162]---> BDD-cost:   17
c ---[1161]---> BDD-cost:    1
c ---[1160]---> BDD-cost:    1
c ---[1159]---> BDD-cost:   17
c ---[1158]---> BDD-cost:   17
c ---[1157]---> BDD-cost:    1
c ---[1156]---> BDD-cost:    1
c ---[1155]---> BDD-cost:   17
c ---[1154]---> BDD-cost:   17
c ---[1153]---> BDD-cost:    1
c ---[1152]---> BDD-cost:    1
c ---[1151]---> BDD-cost:   17
c ---[1150]---> BDD-cost:   17
c ---[1149]---> BDD-cost:    1
c ---[1148]---> BDD-cost:    1
c ---[1147]---> BDD-cost:   17
c ---[1146]---> BDD-cost:   17
c ---[1145]---> BDD-cost:    1
c ---[1144]---> BDD-cost:    1
c ---[1143]---> BDD-cost:   17
c ---[1142]---> BDD-cost:   17
c ---[1141]---> BDD-cost:    1
c ---[1140]---> BDD-cost:    1
c ---[1139]---> BDD-cost:   17
c ---[1138]---> BDD-cost:   17
c ---[1137]---> BDD-cost:    1
c ---[1136]---> BDD-cost:    1
c ---[1135]---> BDD-cost:   17
c ---[1134]---> BDD-cost:   17
c ---[1133]---> BDD-cost:    1
c ---[1132]---> BDD-cost:    1
c ---[1131]---> BDD-cost:   17
c ---[1130]---> BDD-cost:   17
c ---[1129]---> BDD-cost:    1
c ---[1128]---> BDD-cost:    1
c ---[1127]---> BDD-cost:   17
c ---[1126]---> BDD-cost:   17
c ---[1125]---> BDD-cost:    1
c ---[1124]---> BDD-cost:    1
c ---[1123]---> BDD-cost:   17
c ---[1122]---> BDD-cost:   17
c ---[1121]---> BDD-cost:    1
c ---[1120]---> BDD-cost:    1
c ---[1119]---> BDD-cost:   17
c ---[1118]---> BDD-cost:   17
c ---[1117]---> BDD-cost:    1
c ---[1116]---> BDD-cost:    1
c ---[1115]---> BDD-cost:   17
c ---[1114]---> BDD-cost:   17
c ---[1113]---> BDD-cost:    1
c ---[1112]---> BDD-cost:    1
c ---[1111]---> BDD-cost:   17
c ---[1110]---> BDD-cost:   17
c ---[1109]---> BDD-cost:    1
c ---[1108]---> BDD-cost:    1
c ---[1107]---> BDD-cost:   17
c ---[1106]---> BDD-cost:   17
c ---[1105]---> BDD-cost:    1
c ---[1104]---> BDD-cost:    1
c ---[1103]---> BDD-cost:   17
c ---[1102]---> BDD-cost:   17
c ---[1101]---> BDD-cost:    1
c ---[1100]---> BDD-cost:    1
c ---[1099]---> BDD-cost:   17
c ---[1098]---> BDD-cost:   17
c ---[1097]---> BDD-cost:    1
c ---[1096]---> BDD-cost:    1
c ---[1095]---> BDD-cost:   17
c ---[1094]---> BDD-cost:   17
c ---[1093]---> BDD-cost:    1
c ---[1092]---> BDD-cost:    1
c ---[1091]---> BDD-cost:   17
c ---[1090]---> BDD-cost:   17
c ---[1089]---> BDD-cost:    1
c ---[1088]---> BDD-cost:    1
c ---[1087]---> BDD-cost:   17
c ---[1086]---> BDD-cost:   17
c ---[1085]---> BDD-cost:    1
c ---[1084]---> BDD-cost:    1
c ---[1083]---> BDD-cost:   17
c ---[1082]---> BDD-cost:   17
c ---[1081]---> BDD-cost:    1
c ---[1080]---> BDD-cost:    1
c ---[1079]---> BDD-cost:   17
c ---[1078]---> BDD-cost:   17
c ---[1077]---> BDD-cost:    1
c ---[1076]---> BDD-cost:    1
c ---[1075]---> BDD-cost:   17
c ---[1074]---> BDD-cost:   17
c ---[1073]---> BDD-cost:    1
c ---[1072]---> BDD-cost:    1
c ---[1071]---> BDD-cost:   17
c ---[1070]---> BDD-cost:   17
c ---[1069]---> BDD-cost:    1
c ---[1068]---> BDD-cost:    1
c ---[1067]---> BDD-cost:   17
c ---[1066]---> BDD-cost:   17
c ---[1065]---> BDD-cost:    1
c ---[1064]---> BDD-cost:    1
c ---[1063]---> BDD-cost:   17
c ---[1062]---> BDD-cost:   17
c ---[1061]---> BDD-cost:    1
c ---[1060]---> BDD-cost:    1
c ---[1059]---> BDD-cost:   17
c ---[1058]---> BDD-cost:   17
c ---[1057]---> BDD-cost:    1
c ---[1056]---> BDD-cost:    1
c ---[1055]---> BDD-cost:   17
c ---[1054]---> BDD-cost:   17
c ---[1053]---> BDD-cost:    1
c ---[1052]---> BDD-cost:    1
c ---[1051]---> BDD-cost:   17
c ---[1050]---> BDD-cost:   17
c ---[1049]---> BDD-cost:    1
c ---[1048]---> BDD-cost:    1
c ---[1047]---> BDD-cost:   17
c ---[1046]---> BDD-cost:   17
c ---[1045]---> BDD-cost:    1
c ---[1044]---> BDD-cost:    1
c ---[1043]---> BDD-cost:   17
c ---[1042]---> BDD-cost:   17
c ---[1041]---> BDD-cost:    1
c ---[1040]---> BDD-cost:    1
c ---[1039]---> BDD-cost:   17
c ---[1038]---> BDD-cost:   17
c ---[1037]---> BDD-cost:    1
c ---[1036]---> BDD-cost:    1
c ---[1035]---> BDD-cost:   17
c ---[1034]---> BDD-cost:   17
c ---[1033]---> BDD-cost:    1
c ---[1032]---> BDD-cost:    1
c ---[1031]---> BDD-cost:   17
c ---[1030]---> BDD-cost:   17
c ---[1029]---> BDD-cost:    1
c ---[1028]---> BDD-cost:    1
c ---[1027]---> BDD-cost:   17
c ---[1026]---> BDD-cost:   17
c ---[1025]---> BDD-cost:    1
c ---[1024]---> BDD-cost:    1
c ---[1023]---> BDD-cost:   17
c ---[1022]---> BDD-cost:   17
c ---[1021]---> BDD-cost:    1
c ---[1020]---> BDD-cost:    1
c ---[1019]---> BDD-cost:   17
c ---[1018]---> BDD-cost:   17
c ---[1017]---> BDD-cost:    1
c ---[1016]---> BDD-cost:    1
c ---[1015]---> BDD-cost:   17
c ---[1014]---> BDD-cost:   17
c ---[1013]---> BDD-cost:    1
c ---[1012]---> BDD-cost:    1
c ---[1011]---> BDD-cost:   17
c ---[1010]---> BDD-cost:   17
c ---[1009]---> BDD-cost:    1
c ---[1008]---> BDD-cost:    1
c ---[1007]---> BDD-cost:   17
c ---[1006]---> BDD-cost:   17
c ---[1005]---> BDD-cost:    1
c ---[1004]---> BDD-cost:    1
c ---[1003]---> BDD-cost:   17
c ---[1002]---> BDD-cost:   17
c ---[1001]---> BDD-cost:    1
c ---[1000]---> BDD-cost:    1
c ---[ 999]---> BDD-cost:   17
c ---[ 998]---> BDD-cost:   17
c ---[ 997]---> BDD-cost:    1
c ---[ 996]---> BDD-cost:    1
c ---[ 995]---> BDD-cost:   17
c ---[ 994]---> BDD-cost:   17
c ---[ 993]---> BDD-cost:    1
c ---[ 992]---> BDD-cost:    1
c ---[ 991]---> BDD-cost:   17
c ---[ 990]---> BDD-cost:   17
c ---[ 989]---> BDD-cost:    1
c ---[ 988]---> BDD-cost:    1
c ---[ 987]---> BDD-cost:   17
c ---[ 986]---> BDD-cost:   17
c ---[ 985]---> BDD-cost:    1
c ---[ 984]---> BDD-cost:    1
c ---[ 983]---> BDD-cost:   17
c ---[ 982]---> BDD-cost:   17
c ---[ 981]---> BDD-cost:    1
c ---[ 980]---> BDD-cost:    1
c ---[ 979]---> BDD-cost:   17
c ---[ 978]---> BDD-cost:   17
c ---[ 977]---> BDD-cost:    1
c ---[ 976]---> BDD-cost:    1
c ---[ 975]---> BDD-cost:   17
c ---[ 974]---> BDD-cost:   17
c ---[ 973]---> BDD-cost:    1
c ---[ 972]---> BDD-cost:    1
c ---[ 971]---> BDD-cost:   17
c ---[ 970]---> BDD-cost:   17
c ---[ 969]---> BDD-cost:    1
c ---[ 968]---> BDD-cost:    1
c ---[ 967]---> BDD-cost:   21
c ---[ 966]---> BDD-cost:    1
c ---[ 965]---> BDD-cost:    1
c ---[ 964]---> BDD-cost:    1
c ---[ 963]---> BDD-cost:   21
c ---[ 962]---> BDD-cost:    1
c ---[ 961]---> BDD-cost:    1
c ---[ 960]---> BDD-cost:    1
c ---[ 959]---> BDD-cost:   21
c ---[ 958]---> BDD-cost:    1
c ---[ 957]---> BDD-cost:    1
c ---[ 956]---> BDD-cost:    1
c ---[ 955]---> BDD-cost:   21
c ---[ 954]---> BDD-cost:    1
c ---[ 953]---> BDD-cost:    1
c ---[ 952]---> BDD-cost:    1
c ---[ 951]---> BDD-cost:    1
c ---[ 950]---> BDD-cost:    1
c ---[ 949]---> BDD-cost:    1
c ---[ 948]---> BDD-cost:    1
c ---[ 947]---> BDD-cost:    1
c ---[ 946]---> BDD-cost:    1
c ---[ 945]---> BDD-cost:    1
c ---[ 944]---> BDD-cost:    1
c ---[ 943]---> BDD-cost:   21
c ---[ 942]---> BDD-cost:    1
c ---[ 941]---> BDD-cost:    1
c ---[ 940]---> BDD-cost:    1
c ---[ 939]---> BDD-cost:   21
c ---[ 938]---> BDD-cost:    1
c ---[ 937]---> BDD-cost:    1
c ---[ 936]---> BDD-cost:    1
c ---[ 935]---> BDD-cost:   21
c ---[ 934]---> BDD-cost:    1
c ---[ 933]---> BDD-cost:    1
c ---[ 932]---> BDD-cost:    1
c ---[ 931]---> BDD-cost:   21
c ---[ 930]---> BDD-cost:    1
c ---[ 929]---> BDD-cost:    1
c ---[ 928]---> BDD-cost:    1
c ---[ 927]---> BDD-cost:   21
c ---[ 926]---> BDD-cost:    1
c ---[ 925]---> BDD-cost:    1
c ---[ 924]---> BDD-cost:    1
c ---[ 923]---> BDD-cost:   21
c ---[ 922]---> BDD-cost:    1
c ---[ 921]---> BDD-cost:    1
c ---[ 920]---> BDD-cost:    1
c ---[ 919]---> BDD-cost:   17
c ---[ 918]---> BDD-cost:   17
c ---[ 917]---> BDD-cost:    1
c ---[ 916]---> BDD-cost:    1
c ---[ 915]---> BDD-cost:   17
c ---[ 914]---> BDD-cost:   17
c ---[ 913]---> BDD-cost:    1
c ---[ 912]---> BDD-cost:    1
c ---[ 911]---> BDD-cost:   24
c ---[ 910]---> BDD-cost:   17
c ---[ 909]---> BDD-cost:    1
c ---[ 908]---> BDD-cost:    1
c ---[ 907]---> BDD-cost:    1
c ---[ 906]---> BDD-cost:   14
c ---[ 905]---> BDD-cost:    1
c ---[ 904]---> BDD-cost:    1
c ---[ 903]---> BDD-cost:   24
c ---[ 902]---> BDD-cost:   17
c ---[ 901]---> BDD-cost:    1
c ---[ 900]---> BDD-cost:    1
c ---[ 899]---> BDD-cost:    1
c ---[ 898]---> BDD-cost:   14
c ---[ 897]---> BDD-cost:    1
c ---[ 896]---> BDD-cost:    1
c ---[ 895]---> BDD-cost:   17
c ---[ 894]---> BDD-cost:   17
c ---[ 893]---> BDD-cost:    1
c ---[ 892]---> BDD-cost:    1
c ---[ 891]---> BDD-cost:   17
c ---[ 890]---> BDD-cost:   17
c ---[ 889]---> BDD-cost:    1
c ---[ 888]---> BDD-cost:    1
c ---[ 887]---> BDD-cost:   24
c ---[ 886]---> BDD-cost:   17
c ---[ 885]---> BDD-cost:    1
c ---[ 884]---> BDD-cost:    1
c ---[ 883]---> BDD-cost:    1
c ---[ 882]---> BDD-cost:   14
c ---[ 881]---> BDD-cost:    1
c ---[ 880]---> BDD-cost:    1
c ---[ 879]---> BDD-cost:   24
c ---[ 878]---> BDD-cost:   17
c ---[ 877]---> BDD-cost:    1
c ---[ 876]---> BDD-cost:    1
c ---[ 875]---> BDD-cost:    1
c ---[ 874]---> BDD-cost:   14
c ---[ 873]---> BDD-cost:    1
c ---[ 872]---> BDD-cost:    1
c ---[ 871]---> BDD-cost:   21
c ---[ 870]---> BDD-cost:    1
c ---[ 869]---> BDD-cost:    1
c ---[ 868]---> BDD-cost:    1
c ---[ 867]---> BDD-cost:   21
c ---[ 866]---> BDD-cost:    1
c ---[ 865]---> BDD-cost:    1
c ---[ 864]---> BDD-cost:    1
c ---[ 863]---> BDD-cost:   21
c ---[ 862]---> BDD-cost:    1
c ---[ 861]---> BDD-cost:    1
c ---[ 860]---> BDD-cost:    1
c ---[ 859]---> BDD-cost:   21
c ---[ 858]---> BDD-cost:    1
c ---[ 857]---> BDD-cost:    1
c ---[ 856]---> BDD-cost:    1
c ---[ 855]---> BDD-cost:   21
c ---[ 854]---> BDD-cost:    1
c ---[ 853]---> BDD-cost:    1
c ---[ 852]---> BDD-cost:    1
c ---[ 851]---> BDD-cost:   21
c ---[ 850]---> BDD-cost:    1
c ---[ 849]---> BDD-cost:    1
c ---[ 848]---> BDD-cost:    1
c ---[ 847]---> BDD-cost:    1
c ---[ 846]---> BDD-cost:    1
c ---[ 845]---> BDD-cost:    1
c ---[ 844]---> BDD-cost:    1
c ---[ 843]---> BDD-cost:    1
c ---[ 842]---> BDD-cost:    1
c ---[ 841]---> BDD-cost:    1
c ---[ 840]---> BDD-cost:    1
c ---[ 839]---> BDD-cost:   21
c ---[ 838]---> BDD-cost:    1
c ---[ 837]---> BDD-cost:    1
c ---[ 836]---> BDD-cost:    1
c ---[ 835]---> BDD-cost:   21
c ---[ 834]---> BDD-cost:    1
c ---[ 833]---> BDD-cost:    1
c ---[ 832]---> BDD-cost:    1
c ---[ 831]---> BDD-cost:   21
c ---[ 830]---> BDD-cost:    1
c ---[ 829]---> BDD-cost:    1
c ---[ 828]---> BDD-cost:    1
c ---[ 827]---> BDD-cost:   21
c ---[ 826]---> BDD-cost:    1
c ---[ 825]---> BDD-cost:    1
c ---[ 824]---> BDD-cost:    1
c ---[ 823]---> BDD-cost:   17
c ---[ 822]---> BDD-cost:   17
c ---[ 821]---> BDD-cost:    1
c ---[ 820]---> BDD-cost:    1
c ---[ 819]---> BDD-cost:   24
c ---[ 818]---> BDD-cost:   17
c ---[ 817]---> BDD-cost:    1
c ---[ 816]---> BDD-cost:    1
c ---[ 815]---> BDD-cost:    1
c ---[ 814]---> BDD-cost:   14
c ---[ 813]---> BDD-cost:    1
c ---[ 812]---> BDD-cost:    1
c ---[ 811]---> BDD-cost:   21
c ---[ 810]---> BDD-cost:    1
c ---[ 809]---> BDD-cost:    1
c ---[ 808]---> BDD-cost:    1
c ---[ 807]---> BDD-cost:   21
c ---[ 806]---> BDD-cost:    1
c ---[ 805]---> BDD-cost:    1
c ---[ 804]---> BDD-cost:    1
c ---[ 803]---> BDD-cost:   21
c ---[ 802]---> BDD-cost:    1
c ---[ 801]---> BDD-cost:    1
c ---[ 800]---> BDD-cost:    1
c ---[ 799]---> BDD-cost:   17
c ---[ 798]---> BDD-cost:   17
c ---[ 797]---> BDD-cost:    1
c ---[ 796]---> BDD-cost:    1
c ---[ 795]---> BDD-cost:   24
c ---[ 794]---> BDD-cost:   17
c ---[ 793]---> BDD-cost:    1
c ---[ 792]---> BDD-cost:    1
c ---[ 791]---> BDD-cost:    1
c ---[ 790]---> BDD-cost:   14
c ---[ 789]---> BDD-cost:    1
c ---[ 788]---> BDD-cost:    1
c ---[ 787]---> BDD-cost:   21
c ---[ 786]---> BDD-cost:    1
c ---[ 785]---> BDD-cost:    1
c ---[ 784]---> BDD-cost:    1
c ---[ 783]---> BDD-cost:   21
c ---[ 782]---> BDD-cost:    1
c ---[ 781]---> BDD-cost:    1
c ---[ 780]---> BDD-cost:    1
c ---[ 779]---> BDD-cost:   21
c ---[ 778]---> BDD-cost:    1
c ---[ 777]---> BDD-cost:    1
c ---[ 776]---> BDD-cost:    1
c ---[ 775]---> BDD-cost:   16
c ---[ 774]---> BDD-cost:    1
c ---[ 773]---> BDD-cost:    1
c ---[ 772]---> BDD-cost:    1
c ---[ 771]---> BDD-cost:   16
c ---[ 770]---> BDD-cost:    1
c ---[ 769]---> BDD-cost:    1
c ---[ 768]---> BDD-cost:    1
c ---[ 767]---> BDD-cost:   16
c ---[ 766]---> BDD-cost:    1
c ---[ 765]---> BDD-cost:    1
c ---[ 764]---> BDD-cost:    1
c ---[ 763]---> BDD-cost:   16
c ---[ 762]---> BDD-cost:    1
c ---[ 761]---> BDD-cost:    1
c ---[ 760]---> BDD-cost:    1
c ---[ 759]---> BDD-cost:   16
c ---[ 758]---> BDD-cost:    1
c ---[ 757]---> BDD-cost:    1
c ---[ 756]---> BDD-cost:    1
c ---[ 755]---> BDD-cost:   16
c ---[ 754]---> BDD-cost:    1
c ---[ 753]---> BDD-cost:    1
c ---[ 752]---> BDD-cost:    1
c ---[ 751]---> BDD-cost:   16
c ---[ 750]---> BDD-cost:    1
c ---[ 749]---> BDD-cost:    1
c ---[ 748]---> BDD-cost:    1
c ---[ 747]---> BDD-cost:   16
c ---[ 746]---> BDD-cost:    1
c ---[ 745]---> BDD-cost:    1
c ---[ 744]---> BDD-cost:    1
c ---[ 743]---> BDD-cost:    1
c ---[ 742]---> BDD-cost:    1
c ---[ 741]---> BDD-cost:    1
c ---[ 740]---> BDD-cost:    1
c ---[ 739]---> BDD-cost:    1
c ---[ 738]---> BDD-cost:    1
c ---[ 737]---> BDD-cost:    1
c ---[ 736]---> BDD-cost:    1
c ---[ 735]---> BDD-cost:   16
c ---[ 734]---> BDD-cost:    1
c ---[ 733]---> BDD-cost:    1
c ---[ 732]---> BDD-cost:    1
c ---[ 731]---> BDD-cost:   16
c ---[ 730]---> BDD-cost:    1
c ---[ 729]---> BDD-cost:    1
c ---[ 728]---> BDD-cost:    1
c ---[ 727]---> BDD-cost:   17
c ---[ 726]---> BDD-cost:   17
c ---[ 725]---> BDD-cost:    1
c ---[ 724]---> BDD-cost:    1
c ---[ 723]---> BDD-cost:   24
c ---[ 722]---> BDD-cost:   17
c ---[ 721]---> BDD-cost:    1
c ---[ 720]---> BDD-cost:    1
c ---[ 719]---> BDD-cost:    1
c ---[ 718]---> BDD-cost:   14
c ---[ 717]---> BDD-cost:    1
c ---[ 716]---> BDD-cost:    1
c ---[ 715]---> BDD-cost:   21
c ---[ 714]---> BDD-cost:    1
c ---[ 713]---> BDD-cost:    1
c ---[ 712]---> BDD-cost:    1
c ---[ 711]---> BDD-cost:   16
c ---[ 710]---> BDD-cost:    1
c ---[ 709]---> BDD-cost:    1
c ---[ 708]---> BDD-cost:    1
c ---[ 707]---> BDD-cost:   16
c ---[ 706]---> BDD-cost:    1
c ---[ 705]---> BDD-cost:    1
c ---[ 704]---> BDD-cost:    1
c ---[ 703]---> BDD-cost:   16
c ---[ 702]---> BDD-cost:    1
c ---[ 701]---> BDD-cost:    1
c ---[ 700]---> BDD-cost:    1
c ---[ 699]---> BDD-cost:   16
c ---[ 698]---> BDD-cost:    1
c ---[ 697]---> BDD-cost:    1
c ---[ 696]---> BDD-cost:    1
c ---[ 695]---> BDD-cost:   17
c ---[ 694]---> BDD-cost:   17
c ---[ 693]---> BDD-cost:    1
c ---[ 692]---> BDD-cost:    1
c ---[ 691]---> BDD-cost:   24
c ---[ 690]---> BDD-cost:   17
c ---[ 689]---> BDD-cost:    1
c ---[ 688]---> BDD-cost:    1
c ---[ 687]---> BDD-cost:    1
c ---[ 686]---> BDD-cost:   14
c ---[ 685]---> BDD-cost:    1
c ---[ 684]---> BDD-cost:    1
c ---[ 683]---> BDD-cost:   21
c ---[ 682]---> BDD-cost:    1
c ---[ 681]---> BDD-cost:    1
c ---[ 680]---> BDD-cost:    1
c ---[ 679]---> BDD-cost:   16
c ---[ 678]---> BDD-cost:    1
c ---[ 677]---> BDD-cost:    1
c ---[ 676]---> BDD-cost:    1
c ---[ 675]---> BDD-cost:   16
c ---[ 674]---> BDD-cost:    1
c ---[ 673]---> BDD-cost:    1
c ---[ 672]---> BDD-cost:    1
c ---[ 671]---> BDD-cost:   16
c ---[ 670]---> BDD-cost:    1
c ---[ 669]---> BDD-cost:    1
c ---[ 668]---> BDD-cost:    1
c ---[ 667]---> BDD-cost:   16
c ---[ 666]---> BDD-cost:    1
c ---[ 665]---> BDD-cost:    1
c ---[ 664]---> BDD-cost:    1
c ---[ 663]---> BDD-cost:   16
c ---[ 662]---> BDD-cost:    1
c ---[ 661]---> BDD-cost:    1
c ---[ 660]---> BDD-cost:    1
c ---[ 659]---> BDD-cost:   16
c ---[ 658]---> BDD-cost:    1
c ---[ 657]---> BDD-cost:    1
c ---[ 656]---> BDD-cost:    1
c ---[ 655]---> BDD-cost:   16
c ---[ 654]---> BDD-cost:    1
c ---[ 653]---> BDD-cost:    1
c ---[ 652]---> BDD-cost:    1
c ---[ 651]---> BDD-cost:   16
c ---[ 650]---> BDD-cost:    1
c ---[ 649]---> BDD-cost:    1
c ---[ 648]---> BDD-cost:    1
c ---[ 647]---> BDD-cost:   16
c ---[ 646]---> BDD-cost:    1
c ---[ 645]---> BDD-cost:    1
c ---[ 644]---> BDD-cost:    1
c ---[ 643]---> BDD-cost:   16
c ---[ 642]---> BDD-cost:    1
c ---[ 641]---> BDD-cost:    1
c ---[ 640]---> BDD-cost:    1
c ---[ 639]---> BDD-cost:   16
c ---[ 638]---> BDD-cost:    1
c ---[ 637]---> BDD-cost:    1
c ---[ 636]---> BDD-cost:    1
c ---[ 635]---> BDD-cost:   16
c ---[ 634]---> BDD-cost:    1
c ---[ 633]---> BDD-cost:    1
c ---[ 632]---> BDD-cost:    1
c ---[ 631]---> BDD-cost:   16
c ---[ 630]---> BDD-cost:    1
c ---[ 629]---> BDD-cost:    1
c ---[ 628]---> BDD-cost:    1
c ---[ 627]---> BDD-cost:   16
c ---[ 626]---> BDD-cost:    1
c ---[ 625]---> BDD-cost:    1
c ---[ 624]---> BDD-cost:    1
c ---[ 623]---> BDD-cost:    1
c ---[ 622]---> BDD-cost:    1
c ---[ 621]---> BDD-cost:    1
c ---[ 620]---> BDD-cost:    1
c ---[ 619]---> BDD-cost:    1
c ---[ 618]---> BDD-cost:    1
c ---[ 617]---> BDD-cost:    1
c ---[ 616]---> BDD-cost:    1
c ---[ 615]---> BDD-cost:   17
c ---[ 614]---> BDD-cost:   17
c ---[ 613]---> BDD-cost:    1
c ---[ 612]---> BDD-cost:    1
c ---[ 611]---> BDD-cost:   24
c ---[ 610]---> BDD-cost:   17
c ---[ 609]---> BDD-cost:    1
c ---[ 608]---> BDD-cost:    1
c ---[ 607]---> BDD-cost:    1
c ---[ 606]---> BDD-cost:   14
c ---[ 605]---> BDD-cost:    1
c ---[ 604]---> BDD-cost:    1
c ---[ 603]---> BDD-cost:   21
c ---[ 602]---> BDD-cost:    1
c ---[ 601]---> BDD-cost:    1
c ---[ 600]---> BDD-cost:    1
c ---[ 599]---> BDD-cost:   16
c ---[ 598]---> BDD-cost:    1
c ---[ 597]---> BDD-cost:    1
c ---[ 596]---> BDD-cost:    1
c ---[ 595]---> BDD-cost:   16
c ---[ 594]---> BDD-cost:    1
c ---[ 593]---> BDD-cost:    1
c ---[ 592]---> BDD-cost:    1
c ---[ 591]---> BDD-cost:   16
c ---[ 590]---> BDD-cost:    1
c ---[ 589]---> BDD-cost:    1
c ---[ 588]---> BDD-cost:    1
c ---[ 587]---> BDD-cost:   16
c ---[ 586]---> BDD-cost:    1
c ---[ 585]---> BDD-cost:    1
c ---[ 584]---> BDD-cost:    1
c ---[ 583]---> BDD-cost:   16
c ---[ 582]---> BDD-cost:    1
c ---[ 581]---> BDD-cost:    1
c ---[ 580]---> BDD-cost:    1
c ---[ 579]---> BDD-cost:   16
c ---[ 578]---> BDD-cost:    1
c ---[ 577]---> BDD-cost:    1
c ---[ 576]---> BDD-cost:    1
c ---[ 575]---> BDD-cost:   17
c ---[ 574]---> BDD-cost:   17
c ---[ 573]---> BDD-cost:    1
c ---[ 572]---> BDD-cost:    1
c ---[ 571]---> BDD-cost:   24
c ---[ 570]---> BDD-cost:   17
c ---[ 569]---> BDD-cost:    1
c ---[ 568]---> BDD-cost:    1
c ---[ 567]---> BDD-cost:    1
c ---[ 566]---> BDD-cost:   14
c ---[ 565]---> BDD-cost:    1
c ---[ 564]---> BDD-cost:    1
c ---[ 563]---> BDD-cost:   21
c ---[ 562]---> BDD-cost:    1
c ---[ 561]---> BDD-cost:    1
c ---[ 560]---> BDD-cost:    1
c ---[ 559]---> BDD-cost:   16
c ---[ 558]---> BDD-cost:    1
c ---[ 557]---> BDD-cost:    1
c ---[ 556]---> BDD-cost:    1
c ---[ 555]---> BDD-cost:   16
c ---[ 554]---> BDD-cost:    1
c ---[ 553]---> BDD-cost:    1
c ---[ 552]---> BDD-cost:    1
c ---[ 551]---> BDD-cost:   16
c ---[ 550]---> BDD-cost:    1
c ---[ 549]---> BDD-cost:    1
c ---[ 548]---> BDD-cost:    1
c ---[ 547]---> BDD-cost:   16
c ---[ 546]---> BDD-cost:    1
c ---[ 545]---> BDD-cost:    1
c ---[ 544]---> BDD-cost:    1
c ---[ 543]---> BDD-cost:   16
c ---[ 542]---> BDD-cost:    1
c ---[ 541]---> BDD-cost:    1
c ---[ 540]---> BDD-cost:    1
c ---[ 539]---> BDD-cost:   16
c ---[ 538]---> BDD-cost:    1
c ---[ 537]---> BDD-cost:    1
c ---[ 536]---> BDD-cost:    1
c ---[ 535]---> BDD-cost:   16
c ---[ 534]---> BDD-cost:    1
c ---[ 533]---> BDD-cost:    1
c ---[ 532]---> BDD-cost:    1
c ---[ 531]---> BDD-cost:   16
c ---[ 530]---> BDD-cost:    1
c ---[ 529]---> BDD-cost:    1
c ---[ 528]---> BDD-cost:    1
c ---[ 527]---> BDD-cost:   16
c ---[ 526]---> BDD-cost:    1
c ---[ 525]---> BDD-cost:    1
c ---[ 524]---> BDD-cost:    1
c ---[ 523]---> BDD-cost:   16
c ---[ 522]---> BDD-cost:    1
c ---[ 521]---> BDD-cost:    1
c ---[ 520]---> BDD-cost:    1
c ---[ 519]---> BDD-cost:   16
c ---[ 518]---> BDD-cost:    1
c ---[ 517]---> BDD-cost:    1
c ---[ 516]---> BDD-cost:    1
c ---[ 515]---> BDD-cost:   16
c ---[ 514]---> BDD-cost:    1
c ---[ 513]---> BDD-cost:    1
c ---[ 512]---> BDD-cost:    1
c ---[ 511]---> BDD-cost:   16
c ---[ 510]---> BDD-cost:    1
c ---[ 509]---> BDD-cost:    1
c ---[ 508]---> BDD-cost:    1
c ---[ 507]---> BDD-cost:   16
c ---[ 506]---> BDD-cost:    1
c ---[ 505]---> BDD-cost:    1
c ---[ 504]---> BDD-cost:    1
c ---[ 503]---> BDD-cost:   16
c ---[ 502]---> BDD-cost:    1
c ---[ 501]---> BDD-cost:    1
c ---[ 500]---> BDD-cost:    1
c ---[ 499]---> BDD-cost:   16
c ---[ 498]---> BDD-cost:    1
c ---[ 497]---> BDD-cost:    1
c ---[ 496]---> BDD-cost:    1
c ---[ 495]---> BDD-cost:   16
c ---[ 494]---> BDD-cost:    1
c ---[ 493]---> BDD-cost:    1
c ---[ 492]---> BDD-cost:    1
c ---[ 491]---> BDD-cost:   16
c ---[ 490]---> BDD-cost:    1
c ---[ 489]---> BDD-cost:    1
c ---[ 488]---> BDD-cost:    1
c ---[ 487]---> BDD-cost:    1
c ---[ 486]---> BDD-cost:   16
c ---[ 485]---> BDD-cost:    1
c ---[ 484]---> BDD-cost:    1
c ---[ 483]---> BDD-cost:   16
c ---[ 482]---> BDD-cost:    1
c ---[ 481]---> BDD-cost:    1
c ---[ 480]---> BDD-cost:    1
c ---[ 479]---> BDD-cost:   16
c ---[ 478]---> BDD-cost:    1
c ---[ 477]---> BDD-cost:    1
c ---[ 476]---> BDD-cost:    1
c ---[ 475]---> BDD-cost:   16
c ---[ 474]---> BDD-cost:    1
c ---[ 473]---> BDD-cost:    1
c ---[ 472]---> BDD-cost:    1
c ---[ 471]---> BDD-cost:   16
c ---[ 470]---> BDD-cost:    1
c ---[ 469]---> BDD-cost:    1
c ---[ 468]---> BDD-cost:    1
c ---[ 467]---> BDD-cost:   16
c ---[ 466]---> BDD-cost:    1
c ---[ 465]---> BDD-cost:    1
c ---[ 464]---> BDD-cost:    1
c ---[ 463]---> BDD-cost:   16
c ---[ 462]---> BDD-cost:    1
c ---[ 461]---> BDD-cost:    1
c ---[ 460]---> BDD-cost:    1
c ---[ 459]---> BDD-cost:   16
c ---[ 458]---> BDD-cost:    1
c ---[ 457]---> BDD-cost:    1
c ---[ 456]---> BDD-cost:    1
c ---[ 455]---> BDD-cost:   16
c ---[ 454]---> BDD-cost:    1
c ---[ 453]---> BDD-cost:    1
c ---[ 452]---> BDD-cost:    1
c ---[ 451]---> BDD-cost:   16
c ---[ 450]---> BDD-cost:    1
c ---[ 449]---> BDD-cost:    1
c ---[ 448]---> BDD-cost:    1
c ---[ 447]---> BDD-cost:   16
c ---[ 446]---> BDD-cost:    1
c ---[ 445]---> BDD-cost:    1
c ---[ 444]---> BDD-cost:    1
c ---[ 443]---> BDD-cost:   16
c ---[ 442]---> BDD-cost:    1
c ---[ 441]---> BDD-cost:    1
c ---[ 440]---> BDD-cost:    1
c ---[ 439]---> BDD-cost:   16
c ---[ 438]---> BDD-cost:    1
c ---[ 437]---> BDD-cost:    1
c ---[ 436]---> BDD-cost:    1
c ---[ 435]---> BDD-cost:   17
c ---[ 434]---> BDD-cost:   17
c ---[ 433]---> BDD-cost:    1
c ---[ 432]---> BDD-cost:    1
c ---[ 431]---> BDD-cost:   24
c ---[ 430]---> BDD-cost:   17
c ---[ 429]---> BDD-cost:    1
c ---[ 428]---> BDD-cost:    1
c ---[ 427]---> BDD-cost:    1
c ---[ 426]---> BDD-cost:   14
c ---[ 425]---> BDD-cost:    1
c ---[ 424]---> BDD-cost:    1
c ---[ 423]---> BDD-cost:   21
c ---[ 422]---> BDD-cost:    1
c ---[ 421]---> BDD-cost:    1
c ---[ 420]---> BDD-cost:    1
c ---[ 419]---> BDD-cost:   16
c ---[ 418]---> BDD-cost:    1
c ---[ 417]---> BDD-cost:    1
c ---[ 416]---> BDD-cost:    1
c ---[ 415]---> BDD-cost:   16
c ---[ 414]---> BDD-cost:    1
c ---[ 413]---> BDD-cost:    1
c ---[ 412]---> BDD-cost:    1
c ---[ 411]---> BDD-cost:   16
c ---[ 410]---> BDD-cost:    1
c ---[ 409]---> BDD-cost:    1
c ---[ 408]---> BDD-cost:    1
c ---[ 407]---> BDD-cost:   16
c ---[ 406]---> BDD-cost:    1
c ---[ 405]---> BDD-cost:    1
c ---[ 404]---> BDD-cost:    1
c ---[ 403]---> BDD-cost:   16
c ---[ 402]---> BDD-cost:    1
c ---[ 401]---> BDD-cost:    1
c ---[ 400]---> BDD-cost:    1
c ---[ 399]---> BDD-cost:   16
c ---[ 398]---> BDD-cost:    1
c ---[ 397]---> BDD-cost:    1
c ---[ 396]---> BDD-cost:    1
c ---[ 395]---> BDD-cost:   16
c ---[ 394]---> BDD-cost:    1
c ---[ 393]---> BDD-cost:    1
c ---[ 392]---> BDD-cost:    1
c ---[ 391]---> BDD-cost:   16
c ---[ 390]---> BDD-cost:    1
c ---[ 389]---> BDD-cost:    1
c ---[ 388]---> BDD-cost:    1
c ---[ 387]---> BDD-cost:   17
c ---[ 386]---> BDD-cost:   17
c ---[ 385]---> BDD-cost:    1
c ---[ 384]---> BDD-cost:    1
c ---[ 383]---> BDD-cost:   24
c ---[ 382]---> BDD-cost:   17
c ---[ 381]---> BDD-cost:    1
c ---[ 380]---> BDD-cost:    1
c ---[ 379]---> BDD-cost:    1
c ---[ 378]---> BDD-cost:   14
c ---[ 377]---> BDD-cost:    1
c ---[ 376]---> BDD-cost:    1
c ---[ 375]---> BDD-cost:   21
c ---[ 374]---> BDD-cost:    1
c ---[ 373]---> BDD-cost:    1
c ---[ 372]---> BDD-cost:    1
c ---[ 371]---> BDD-cost:   16
c ---[ 370]---> BDD-cost:    1
c ---[ 369]---> BDD-cost:    1
c ---[ 368]---> BDD-cost:    1
c ---[ 367]---> BDD-cost:   16
c ---[ 366]---> BDD-cost:    1
c ---[ 365]---> BDD-cost:    1
c ---[ 364]---> BDD-cost:    1
c ---[ 363]---> BDD-cost:   16
c ---[ 362]---> BDD-cost:    1
c ---[ 361]---> BDD-cost:    1
c ---[ 360]---> BDD-cost:    1
c ---[ 359]---> BDD-cost:   16
c ---[ 358]---> BDD-cost:    1
c ---[ 357]---> BDD-cost:    1
c ---[ 356]---> BDD-cost:    1
c ---[ 355]---> BDD-cost:   16
c ---[ 354]---> BDD-cost:    1
c ---[ 353]---> BDD-cost:    1
c ---[ 352]---> BDD-cost:    1
c ---[ 351]---> BDD-cost:   16
c ---[ 350]---> BDD-cost:    1
c ---[ 349]---> BDD-cost:    1
c ---[ 348]---> BDD-cost:    1
c ---[ 347]---> BDD-cost:   16
c ---[ 346]---> BDD-cost:    1
c ---[ 345]---> BDD-cost:    1
c ---[ 344]---> BDD-cost:    1
c ---[ 343]---> BDD-cost:   16
c ---[ 342]---> BDD-cost:    1
c ---[ 341]---> BDD-cost:    1
c ---[ 340]---> BDD-cost:    1
c ---[ 339]---> BDD-cost:   14
c ---[ 338]---> BDD-cost:   14
c ---[ 337]---> BDD-cost:    1
c ---[ 336]---> BDD-cost:    1
c ---[ 335]---> BDD-cost:   14
c ---[ 334]---> BDD-cost:   14
c ---[ 333]---> BDD-cost:    1
c ---[ 332]---> BDD-cost:    1
c ---[ 331]---> BDD-cost:   14
c ---[ 330]---> BDD-cost:   14
c ---[ 329]---> BDD-cost:    1
c ---[ 328]---> BDD-cost:    1
c ---[ 327]---> BDD-cost:   14
c ---[ 326]---> BDD-cost:   14
c ---[ 325]---> BDD-cost:    1
c ---[ 324]---> BDD-cost:    1
c ---[ 323]---> BDD-cost:   14
c ---[ 322]---> BDD-cost:   14
c ---[ 321]---> BDD-cost:    1
c ---[ 320]---> BDD-cost:    1
c ---[ 319]---> BDD-cost:   14
c ---[ 318]---> BDD-cost:   14
c ---[ 317]---> BDD-cost:    1
c ---[ 316]---> BDD-cost:    1
c ---[ 315]---> BDD-cost:   17
c ---[ 314]---> BDD-cost:   17
c ---[ 313]---> BDD-cost:    1
c ---[ 312]---> BDD-cost:    1
c ---[ 311]---> BDD-cost:   17
c ---[ 310]---> BDD-cost:   17
c ---[ 309]---> BDD-cost:    1
c ---[ 308]---> BDD-cost:    1
c ---[ 307]---> BDD-cost:   17
c ---[ 306]---> BDD-cost:   17
c ---[ 305]---> BDD-cost:    1
c ---[ 304]---> BDD-cost:    1
c ---[ 303]---> BDD-cost:   21
c ---[ 302]---> BDD-cost:    1
c ---[ 301]---> BDD-cost:    1
c ---[ 300]---> BDD-cost:    1
c ---[ 299]---> BDD-cost:   21
c ---[ 298]---> BDD-cost:    1
c ---[ 297]---> BDD-cost:    1
c ---[ 296]---> BDD-cost:    1
c ---[ 295]---> BDD-cost:   17
c ---[ 294]---> BDD-cost:   17
c ---[ 293]---> BDD-cost:    1
c ---[ 292]---> BDD-cost:    1
c ---[ 291]---> BDD-cost:   21
c ---[ 290]---> BDD-cost:    1
c ---[ 289]---> BDD-cost:    1
c ---[ 288]---> BDD-cost:    1
c ---[ 287]---> BDD-cost:   21
c ---[ 286]---> BDD-cost:    1
c ---[ 285]---> BDD-cost:    1
c ---[ 284]---> BDD-cost:    1
c ---[ 283]---> BDD-cost:   17
c ---[ 282]---> BDD-cost:   17
c ---[ 281]---> BDD-cost:    1
c ---[ 280]---> BDD-cost:    1
c ---[ 279]---> BDD-cost:   21
c ---[ 278]---> BDD-cost:    1
c ---[ 277]---> BDD-cost:    1
c ---[ 276]---> BDD-cost:    1
c ---[ 275]---> BDD-cost:   21
c ---[ 274]---> BDD-cost:    1
c ---[ 273]---> BDD-cost:    1
c ---[ 272]---> BDD-cost:    1
c ---[ 271]---> BDD-cost:   21
c ---[ 270]---> BDD-cost:    1
c ---[ 269]---> BDD-cost:    1
c ---[ 268]---> BDD-cost:    1
c ---[ 267]---> BDD-cost:   21
c ---[ 266]---> BDD-cost:    1
c ---[ 265]---> BDD-cost:    1
c ---[ 264]---> BDD-cost:    1
c ---[ 263]---> BDD-cost:   17
c ---[ 262]---> BDD-cost:   17
c ---[ 261]---> BDD-cost:    1
c ---[ 260]---> BDD-cost:    1
c ---[ 259]---> BDD-cost:   21
c ---[ 258]---> BDD-cost:    1
c ---[ 257]---> BDD-cost:    1
c ---[ 256]---> BDD-cost:    1
c ---[ 255]---> BDD-cost:   21
c ---[ 254]---> BDD-cost:    1
c ---[ 253]---> BDD-cost:    1
c ---[ 252]---> BDD-cost:    1
c ---[ 251]---> BDD-cost:   21
c ---[ 250]---> BDD-cost:    1
c ---[ 249]---> BDD-cost:    1
c ---[ 248]---> BDD-cost:    1
c ---[ 247]---> BDD-cost:   21
c ---[ 246]---> BDD-cost:    1
c ---[ 245]---> BDD-cost:    1
c ---[ 244]---> BDD-cost:    1
c ---[ 243]---> BDD-cost:   17
c ---[ 242]---> BDD-cost:   17
c ---[ 241]---> BDD-cost:    1
c ---[ 240]---> BDD-cost:    1
c ---[ 239]---> BDD-cost:   21
c ---[ 238]---> BDD-cost:    1
c ---[ 237]---> BDD-cost:    1
c ---[ 236]---> BDD-cost:    1
c ---[ 235]---> BDD-cost:   21
c ---[ 234]---> BDD-cost:    1
c ---[ 233]---> BDD-cost:    1
c ---[ 232]---> BDD-cost:    1
c ---[ 231]---> BDD-cost:   16
c ---[ 230]---> BDD-cost:    1
c ---[ 229]---> BDD-cost:    1
c ---[ 228]---> BDD-cost:    1
c ---[ 227]---> BDD-cost:   16
c ---[ 226]---> BDD-cost:    1
c ---[ 225]---> BDD-cost:    1
c ---[ 224]---> BDD-cost:    1
c ---[ 223]---> BDD-cost:   16
c ---[ 222]---> BDD-cost:    1
c ---[ 221]---> BDD-cost:    1
c ---[ 220]---> BDD-cost:    1
c ---[ 219]---> BDD-cost:   16
c ---[ 218]---> BDD-cost:    1
c ---[ 217]---> BDD-cost:    1
c ---[ 216]---> BDD-cost:    1
c ---[ 215]---> BDD-cost:   17
c ---[ 214]---> BDD-cost:   17
c ---[ 213]---> BDD-cost:    1
c ---[ 212]---> BDD-cost:    1
c ---[ 211]---> BDD-cost:   21
c ---[ 210]---> BDD-cost:    1
c ---[ 209]---> BDD-cost:    1
c ---[ 208]---> BDD-cost:    1
c ---[ 207]---> BDD-cost:   21
c ---[ 206]---> BDD-cost:    1
c ---[ 205]---> BDD-cost:    1
c ---[ 204]---> BDD-cost:    1
c ---[ 203]---> BDD-cost:   16
c ---[ 202]---> BDD-cost:    1
c ---[ 201]---> BDD-cost:    1
c ---[ 200]---> BDD-cost:    1
c ---[ 199]---> BDD-cost:   16
c ---[ 198]---> BDD-cost:    1
c ---[ 197]---> BDD-cost:    1
c ---[ 196]---> BDD-cost:    1
c ---[ 195]---> BDD-cost:   16
c ---[ 194]---> BDD-cost:    1
c ---[ 193]---> BDD-cost:    1
c ---[ 192]---> BDD-cost:    1
c ---[ 191]---> BDD-cost:   16
c ---[ 190]---> BDD-cost:    1
c ---[ 189]---> BDD-cost:    1
c ---[ 188]---> BDD-cost:    1
c ---[ 187]---> BDD-cost:   17
c ---[ 186]---> BDD-cost:   17
c ---[ 185]---> BDD-cost:    1
c ---[ 184]---> BDD-cost:    1
c ---[ 183]---> BDD-cost:   21
c ---[ 182]---> BDD-cost:    1
c ---[ 181]---> BDD-cost:    1
c ---[ 180]---> BDD-cost:    1
c ---[ 179]---> BDD-cost:   21
c ---[ 178]---> BDD-cost:    1
c ---[ 177]---> BDD-cost:    1
c ---[ 176]---> BDD-cost:    1
c ---[ 175]---> BDD-cost:   16
c ---[ 174]---> BDD-cost:    1
c ---[ 173]---> BDD-cost:    1
c ---[ 172]---> BDD-cost:    1
c ---[ 171]---> BDD-cost:   16
c ---[ 170]---> BDD-cost:    1
c ---[ 169]---> BDD-cost:    1
c ---[ 168]---> BDD-cost:    1
c ---[ 167]---> BDD-cost:   16
c ---[ 166]---> BDD-cost:    1
c ---[ 165]---> BDD-cost:    1
c ---[ 164]---> BDD-cost:    1
c ---[ 163]---> BDD-cost:   16
c ---[ 162]---> BDD-cost:    1
c ---[ 161]---> BDD-cost:    1
c ---[ 160]---> BDD-cost:    1
c ---[ 159]---> BDD-cost:   16
c ---[ 158]---> BDD-cost:    1
c ---[ 157]---> BDD-cost:    1
c ---[ 156]---> BDD-cost:    1
c ---[ 155]---> BDD-cost:   16
c ---[ 154]---> BDD-cost:    1
c ---[ 153]---> BDD-cost:    1
c ---[ 152]---> BDD-cost:    1
c ---[ 151]---> BDD-cost:   17
c ---[ 150]---> BDD-cost:   17
c ---[ 149]---> BDD-cost:    1
c ---[ 148]---> BDD-cost:    1
c ---[ 147]---> BDD-cost:   21
c ---[ 146]---> BDD-cost:    1
c ---[ 145]---> BDD-cost:    1
c ---[ 144]---> BDD-cost:    1
c ---[ 143]---> BDD-cost:   21
c ---[ 142]---> BDD-cost:    1
c ---[ 141]---> BDD-cost:    1
c ---[ 140]---> BDD-cost:    1
c ---[ 139]---> BDD-cost:   16
c ---[ 138]---> BDD-cost:    1
c ---[ 137]---> BDD-cost:    1
c ---[ 136]---> BDD-cost:    1
c ---[ 135]---> BDD-cost:   16
c ---[ 134]---> BDD-cost:    1
c ---[ 133]---> BDD-cost:    1
c ---[ 132]---> BDD-cost:    1
c ---[ 131]---> BDD-cost:   16
c ---[ 130]---> BDD-cost:    1
c ---[ 129]---> BDD-cost:    1
c ---[ 128]---> BDD-cost:    1
c ---[ 127]---> BDD-cost:   16
c ---[ 126]---> BDD-cost:    1
c ---[ 125]---> BDD-cost:    1
c ---[ 124]---> BDD-cost:    1
c ---[ 123]---> BDD-cost:   16
c ---[ 122]---> BDD-cost:    1
c ---[ 121]---> BDD-cost:    1
c ---[ 120]---> BDD-cost:    1
c ---[ 119]---> BDD-cost:   16
c ---[ 118]---> BDD-cost:    1
c ---[ 117]---> BDD-cost:    1
c ---[ 116]---> BDD-cost:    1
c ---[ 115]---> BDD-cost:   14
c ---[ 114]---> BDD-cost:   14
c ---[ 113]---> BDD-cost:    1
c ---[ 112]---> BDD-cost:    1
c ---[ 111]---> BDD-cost:   14
c ---[ 110]---> BDD-cost:   14
c ---[ 109]---> BDD-cost:    1
c ---[ 108]---> BDD-cost:    1
c ---[ 107]---> BDD-cost:   14
c ---[ 106]---> BDD-cost:   14
c ---[ 105]---> BDD-cost:    1
c ---[ 104]---> BDD-cost:    1
c ---[ 103]---> BDD-cost:   14
c ---[ 102]---> BDD-cost:   14
c ---[ 101]---> BDD-cost:    1
c ---[ 100]---> BDD-cost:    1
c ---[  99]---> BDD-cost:   14
c ---[  98]---> BDD-cost:   14
c ---[  97]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  95]---> BDD-cost:   14
c ---[  94]---> BDD-cost:   14
c ---[  93]---> BDD-cost:    1
c ---[  92]---> BDD-cost:    1
c ---[  91]---> BDD-cost:   14
c ---[  90]---> BDD-cost:   14
c ---[  89]---> BDD-cost:    1
c ---[  88]---> BDD-cost:    1
c ---[  87]---> BDD-cost:   14
c ---[  86]---> BDD-cost:   14
c ---[  85]---> BDD-cost:    1
c ---[  84]---> BDD-cost:    1
c ---[  83]---> BDD-cost:   14
c ---[  82]---> BDD-cost:   14
c ---[  81]---> BDD-cost:    1
c ---[  80]---> BDD-cost:    1
c ---[  79]---> BDD-cost:   14
c ---[  78]---> BDD-cost:   14
c ---[  77]---> BDD-cost:    1
c ---[  76]---> BDD-cost:    1
c ---[  75]---> BDD-cost:   14
c ---[  74]---> BDD-cost:   14
c ---[  73]---> BDD-cost:    1
c ---[  72]---> BDD-cost:    1
c ---[  71]---> BDD-cost:   14
c ---[  70]---> BDD-cost:   14
c ---[  69]---> BDD-cost:    1
c ---[  68]---> BDD-cost:    1
c ---[  67]---> BDD-cost:   14
c ---[  66]---> BDD-cost:   14
c ---[  65]---> BDD-cost:    1
c ---[  64]---> BDD-cost:    1
c ---[  63]---> BDD-cost:   14
c ---[  62]---> BDD-cost:   14
c ---[  61]---> BDD-cost:    1
c ---[  60]---> BDD-cost:    1
c ---[  59]---> BDD-cost:   14
c ---[  58]---> BDD-cost:   14
c ---[  57]---> BDD-cost:    1
c ---[  56]---> BDD-cost:    1
c ---[  55]---> BDD-cost:   14
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:    1
c ---[  52]---> BDD-cost:    1
c ---[  51]---> BDD-cost:   14
c ---[  50]---> BDD-cost:   14
c ---[  49]---> BDD-cost:    1
c ---[  48]---> BDD-cost:    1
c ---[  47]---> BDD-cost:   14
c ---[  46]---> BDD-cost:   14
c ---[  45]---> BDD-cost:    1
c ---[  44]---> BDD-cost:    1
c ---[  43]---> BDD-cost:   14
c ---[  42]---> BDD-cost:   14
c ---[  41]---> BDD-cost:    1
c ---[  40]---> BDD-cost:    1
c ---[  39]---> BDD-cost:   14
c ---[  38]---> BDD-cost:   14
c ---[  37]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    1
c ---[  35]---> BDD-cost:   14
c ---[  34]---> BDD-cost:   14
c ---[  33]---> BDD-cost:    1
c ---[  32]---> BDD-cost:    1
c ---[  31]---> BDD-cost:   14
c ---[  30]---> BDD-cost:   14
c ---[  29]---> BDD-cost:    1
c ---[  28]---> BDD-cost:    1
c ---[  27]---> BDD-cost:   14
c ---[  26]---> BDD-cost:   14
c ---[  25]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:   14
c ---[  22]---> BDD-cost:   14
c ---[  21]---> BDD-cost:    1
c ---[  20]---> BDD-cost:    1
c ---[  19]---> BDD-cost:   14
c ---[  18]---> BDD-cost:   14
c ---[  17]---> BDD-cost:    1
c ---[  16]---> BDD-cost:    1
c ---[  15]---> BDD-cost:   14
c ---[  14]---> BDD-cost:   14
c ---[  13]---> BDD-cost:    1
c ---[  12]---> BDD-cost:    1
c ---[  11]---> BDD-cost:   14
c ---[  10]---> BDD-cost:   14
c ---[   9]---> BDD-cost:    1
c ---[   8]---> BDD-cost:    1
c ---[   7]---> BDD-cost:   14
c ---[   6]---> BDD-cost:   14
c ---[   5]---> BDD-cost:    1
c ---[   4]---> BDD-cost:    1
c ---[   3]---> BDD-cost:   14
c ---[   2]---> BDD-cost:   14
c ---[   1]---> BDD-cost:    1
c ---[   0]---> BDD-cost:    1
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  122857   308719 |   36857       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/37122          
c   -- var.elim.:  2000/37122          
c   -- var.elim.:  3000/37122          
c   -- var.elim.:  4000/37122          
c   -- var.elim.:  5000/37122          
c   -- var.elim.:  6000/37122          
c   -- var.elim.:  7000/37122          
c   -- var.elim.:  8000/37122          
c   -- var.elim.:  9000/37122          
c   -- var.elim.:  10000/37122          
c   -- var.elim.:  11000/37122          
c   -- var.elim.:  12000/37122          
c   -- var.elim.:  13000/37122          
c   -- var.elim.:  14000/37122          
c   -- var.elim.:  15000/37122          
c   -- var.elim.:  16000/37122          
c   -- var.elim.:  17000/37122          
c   -- var.elim.:  18000/37122          
c   -- var.elim.:  19000/37122          
c   -- var.elim.:  20000/37122          
c   -- var.elim.:  21000/37122          
c   -- var.elim.:  22000/37122          
c   -- var.elim.:  23000/37122          
c   -- var.elim.:  24000/37122          
c   -- var.elim.:  25000/37122          
c   -- var.elim.:  26000/37122          
c   -- var.elim.:  27000/37122          
c   -- var.elim.:  28000/37122          
c   -- var.elim.:  29000/37122          
c   -- var.elim.:  30000/37122          
c   -- var.elim.:  31000/37122          
c   -- var.elim.:  32000/37122          
c   -- var.elim.:  33000/37122          
c   -- var.elim.:  34000/37122          
c   -- var.elim.:  35000/37122          
c   -- var.elim.:  36000/37122          
c   -- var.elim.:  37000/37122          
c   -- var.elim.:  37122/37122          
c   -- var.elim.:  1000/12226          
c   -- var.elim.:  2000/12226          
c   -- var.elim.:  3000/12226          
c   -- var.elim.:  4000/12226          
c   -- var.elim.:  5000/12226          
c   -- var.elim.:  6000/12226          
c   -- var.elim.:  7000/12226          
c   -- var.elim.:  8000/12226          
c   -- var.elim.:  9000/12226          
c   -- var.elim.:  10000/12226          
c   -- var.elim.:  11000/12226          
c   -- var.elim.:  12000/12226          
c   -- var.elim.:  12226/12226          
c   -- var.elim.:  1000/1018          
c   -- var.elim.:  1018/1018          
c   -- var.elim.:  318/318          
c   -- var.elim.:  270/270          
c   -- var.elim.:  140/140          
c   -- var.elim.:  38/38          
c   -- var.elim.:  22/22          
c   -- var.elim.:  4/4          
c   -- var.elim.:  10/10          
c   -- subsuming                       
c   -- var.elim.:  1000/4573          
c   -- var.elim.:  2000/4573          
c   -- var.elim.:  3000/4573          
c   -- var.elim.:  4000/4573          
c   -- var.elim.:  4573/4573          
c   -- var.elim.:  1000/1878          
c   -- var.elim.:  1878/1878          
c   -- var.elim.:  236/236          
c   -- var.elim.:  72/72          
c   -- var.elim.:  16/16          
c   -- var.elim.:  8/8          
c   -- subsuming                       
c   -- var.elim.:  303/303          
c   -- var.elim.:  35/35          
c |         0 |   64836   209584 |      --       0       --      -- |     --   | -58021/-95193
c |         0 |   64836   209584 |   25934       0        0     nan |  0.000 % |
c |       100 |   64836   209584 |   28527     100      924     9.2 | 24.549 % |
c |       250 |   64836   209584 |   31380     250     3109    12.4 | 24.549 % |
c |       480 |   64836   209584 |   34518     480     6351    13.2 | 24.550 % |
c |       818 |   64836   209584 |   37970     818    11885    14.5 | 24.549 % |
c |      1325 |   64836   209584 |   41767    1325    54916    41.4 | 24.549 % |
c |      2085 |   64836   209584 |   45944    2085    66340    31.8 | 24.549 % |
c |      3224 |   64836   209584 |   50538    3224   174487    54.1 | 24.549 % |
c |      4935 |   64836   209584 |   55592    4935   241415    48.9 | 24.549 % |
c |      749#### 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.66 0.88 0.88 1/54 28691
Raw data (stat): 28691 (runsolver) R 28690 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480389399 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0011 s]
Raw data (loadavg): 0.71 0.88 0.88 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 7725 0 0 0 973 25 0 0 25 0 1 0 480389399 32833536 7083 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8016 7083 603 41 0 7975 0
vsize: 32064
[startup+20.0016 s]
Raw data (loadavg): 0.75 0.89 0.88 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 8357 0 0 0 1971 27 0 0 25 0 1 0 480389399 35336192 7715 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8627 7715 603 41 0 8586 0
vsize: 34508
[startup+30.0016 s]
Raw data (loadavg): 0.79 0.89 0.88 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 9253 0 0 0 2968 30 0 0 25 0 1 0 480389399 39120896 8611 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9551 8611 603 41 0 9510 0
vsize: 38204
[startup+40.0021 s]
Raw data (loadavg): 0.82 0.89 0.88 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 10833 0 0 0 3963 35 0 0 25 0 1 0 480389399 45592576 10191 4294967295 134512640 134672761 3221224528 3221223712 134615843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 10191 603 41 0 11090 0
vsize: 44524
[startup+50.0024 s]
Raw data (loadavg): 0.85 0.90 0.89 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 11825 0 0 0 4961 37 0 0 25 0 1 0 480389399 49795072 11183 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12157 11183 603 41 0 12116 0
vsize: 48628
[startup+60.0034 s]
Raw data (loadavg): 0.87 0.90 0.89 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 12943 0 0 0 5959 40 0 0 25 0 1 0 480389399 54276096 12301 4294967295 134512640 134672761 3221224528 3221223712 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13251 12301 603 41 0 13210 0
vsize: 53004
[startup+70.0041 s]
Raw data (loadavg): 0.89 0.90 0.89 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 13278 0 0 0 6958 41 0 0 25 0 1 0 480389399 55627776 12636 4294967295 134512640 134672761 3221224528 3221223712 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13581 12636 603 41 0 13540 0
vsize: 54324
[startup+80.0035 s]
Raw data (loadavg): 0.91 0.90 0.89 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 13568 0 0 0 7958 41 0 0 25 0 1 0 480389399 56881152 12926 4294967295 134512640 134672761 3221224528 3221223712 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13887 12926 603 41 0 13846 0
vsize: 55548
[startup+90.0035 s]
Raw data (loadavg): 0.92 0.91 0.89 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 13928 0 0 0 8957 42 0 0 25 0 1 0 480389399 58335232 13286 4294967295 134512640 134672761 3221224528 3221223712 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14242 13286 603 41 0 14201 0
vsize: 56968
[startup+100.003 s]
Raw data (loadavg): 0.93 0.91 0.89 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 15327 0 0 0 9954 45 0 0 25 0 1 0 480389399 63950848 14685 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15613 14685 603 41 0 15572 0
vsize: 62452
[startup+110.004 s]
Raw data (loadavg): 0.94 0.91 0.89 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 16819 0 0 0 10950 50 0 0 25 0 1 0 480389399 70361088 16177 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17178 16177 603 41 0 17137 0
vsize: 68712
[startup+120.005 s]
Raw data (loadavg): 0.95 0.91 0.89 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 18207 0 0 0 11946 53 0 0 25 0 1 0 480389399 76021760 17565 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18560 17565 603 41 0 18519 0
vsize: 74240
[startup+130.004 s]
Raw data (loadavg): 0.96 0.92 0.89 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 19366 0 0 0 12943 56 0 0 25 0 1 0 480389399 80797696 18724 4294967295 134512640 134672761 3221224528 3221223712 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19726 18724 603 41 0 19685 0
vsize: 78904
[startup+140.005 s]
Raw data (loadavg): 0.96 0.92 0.89 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 20573 0 0 0 13941 59 0 0 25 0 1 0 480389399 85696512 19931 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20922 19931 603 41 0 20881 0
vsize: 83688
[startup+150.005 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 21782 0 0 0 14939 62 0 0 25 0 1 0 480389399 90685440 21140 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22140 21140 603 41 0 22099 0
vsize: 88560
[startup+160.005 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 23031 0 0 0 15935 65 0 0 25 0 1 0 480389399 95797248 22389 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23388 22389 603 41 0 23347 0
vsize: 93552
[startup+170.005 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 23972 0 0 0 16933 67 0 0 25 0 1 0 480389399 99737600 23330 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24350 23330 603 41 0 24309 0
vsize: 97400
[startup+180.005 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 25050 0 0 0 17931 70 0 0 25 0 1 0 480389399 104079360 24408 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25410 24408 603 41 0 25369 0
vsize: 101640
[startup+190.005 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 26095 0 0 0 18929 72 0 0 25 0 1 0 480389399 108367872 25453 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26457 25453 603 41 0 26416 0
vsize: 105828
[startup+200.005 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 27356 0 0 0 19926 75 0 0 25 0 1 0 480389399 113577984 26714 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27729 26714 603 41 0 27688 0
vsize: 110916
[startup+210.006 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 28368 0 0 0 20923 79 0 0 25 0 1 0 480389399 117661696 27726 4294967295 134512640 134672761 3221224528 3221223712 134615686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28726 27726 603 41 0 28685 0
vsize: 114904
[startup+220.006 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 29287 0 0 0 21919 82 0 0 25 0 1 0 480389399 121356288 28645 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29628 28645 603 41 0 29587 0
vsize: 118512
[startup+230.006 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 30538 0 0 0 22916 86 0 0 25 0 1 0 480389399 126504960 29896 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30885 29896 603 41 0 30844 0
vsize: 123540
[startup+240.005 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 31572 0 0 0 23914 88 0 0 25 0 1 0 480389399 130732032 30930 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31917 30930 603 41 0 31876 0
vsize: 127668
[startup+250.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 32540 0 0 0 24911 91 0 0 25 0 1 0 480389399 134688768 31898 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32883 31898 603 41 0 32842 0
vsize: 131532
[startup+260.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33179 0 0 0 25910 92 0 0 25 0 1 0 480389399 136933376 32424 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32424 603 41 0 33390 0
vsize: 133724
[startup+270.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33179 0 0 0 26910 92 0 0 25 0 1 0 480389399 136933376 32424 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32424 603 41 0 33390 0
vsize: 133724
[startup+280.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33179 0 0 0 27910 92 0 0 25 0 1 0 480389399 136933376 32424 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32424 603 41 0 33390 0
vsize: 133724
[startup+290.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33179 0 0 0 28911 92 0 0 25 0 1 0 480389399 136933376 32424 4294967295 134512640 134672761 3221224528 3221223712 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32424 603 41 0 33390 0
vsize: 133724
[startup+300.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33179 0 0 0 29911 92 0 0 25 0 1 0 480389399 136933376 32424 4294967295 134512640 134672761 3221224528 3221223568 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32424 603 41 0 33390 0
vsize: 133724
[startup+310.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33179 0 0 0 30911 92 0 0 25 0 1 0 480389399 136933376 32424 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32424 603 41 0 33390 0
vsize: 133724
[startup+320.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33180 0 0 0 31911 92 0 0 25 0 1 0 480389399 136933376 32425 4294967295 134512640 134672761 3221224528 3221223728 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32425 603 41 0 33390 0
vsize: 133724
[startup+330.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33181 0 0 0 32911 92 0 0 25 0 1 0 480389399 136933376 32426 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32426 603 41 0 33390 0
vsize: 133724
[startup+340.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33182 0 0 0 33912 92 0 0 25 0 1 0 480389399 136933376 32427 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32427 603 41 0 33390 0
vsize: 133724
[startup+350.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33183 0 0 0 34912 92 0 0 25 0 1 0 480389399 136933376 32428 4294967295 134512640 134672761 3221224528 3221223680 134614555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32428 603 41 0 33390 0
vsize: 133724
[startup+360.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33186 0 0 0 35912 92 0 0 25 0 1 0 480389399 136933376 32431 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32431 603 41 0 33390 0
vsize: 133724
[startup+370.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33189 0 0 0 36912 92 0 0 25 0 1 0 480389399 136933376 32434 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32434 603 41 0 33390 0
vsize: 133724
[startup+380.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33189 0 0 0 37912 92 0 0 25 0 1 0 480389399 136933376 32434 4294967295 134512640 134672761 3221224528 3221223712 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32434 603 41 0 33390 0
vsize: 133724
[startup+390.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33189 0 0 0 38913 92 0 0 25 0 1 0 480389399 136933376 32434 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32434 603 41 0 33390 0
vsize: 133724
[startup+400.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33189 0 0 0 39913 92 0 0 25 0 1 0 480389399 136933376 32434 4294967295 134512640 134672761 3221224528 3221223712 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32434 603 41 0 33390 0
vsize: 133724
[startup+410.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33190 0 0 0 40913 92 0 0 25 0 1 0 480389399 136933376 32435 4294967295 134512640 134672761 3221224528 3221223712 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32435 603 41 0 33390 0
vsize: 133724
[startup+420.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33192 0 0 0 41913 92 0 0 25 0 1 0 480389399 136933376 32437 4294967295 134512640 134672761 3221224528 3221223712 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32437 603 41 0 33390 0
vsize: 133724
[startup+430.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33193 0 0 0 42913 92 0 0 25 0 1 0 480389399 136933376 32438 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32438 603 41 0 33390 0
vsize: 133724
[startup+440.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33193 0 0 0 43914 92 0 0 25 0 1 0 480389399 136933376 32438 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32438 603 41 0 33390 0
vsize: 133724
[startup+450.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33193 0 0 0 44914 92 0 0 25 0 1 0 480389399 136933376 32438 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32438 603 41 0 33390 0
vsize: 133724
[startup+460.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33193 0 0 0 45914 92 0 0 25 0 1 0 480389399 136933376 32438 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32438 603 41 0 33390 0
vsize: 133724
[startup+470.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33196 0 0 0 46914 92 0 0 25 0 1 0 480389399 136933376 32441 4294967295 134512640 134672761 3221224528 3221223712 134615581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32441 603 41 0 33390 0
vsize: 133724
[startup+480.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33198 0 0 0 47914 92 0 0 25 0 1 0 480389399 136933376 32443 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32443 603 41 0 33390 0
vsize: 133724
[startup+490.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33200 0 0 0 48915 92 0 0 25 0 1 0 480389399 136933376 32445 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32445 603 41 0 33390 0
vsize: 133724
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33203 0 0 0 49915 92 0 0 25 0 1 0 480389399 136933376 32448 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32448 603 41 0 33390 0
vsize: 133724
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33206 0 0 0 50915 92 0 0 25 0 1 0 480389399 136933376 32451 4294967295 134512640 134672761 3221224528 3221223568 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33431 32451 603 41 0 33390 0
vsize: 133724
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33210 0 0 0 51915 92 0 0 25 0 1 0 480389399 137457664 32455 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33559 32455 603 41 0 33518 0
vsize: 134236
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33212 0 0 0 52915 93 0 0 25 0 1 0 480389399 137457664 32457 4294967295 134512640 134672761 3221224528 3221223712 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33559 32457 603 41 0 33518 0
vsize: 134236
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33215 0 0 0 53916 93 0 0 25 0 1 0 480389399 137457664 32460 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33559 32460 603 41 0 33518 0
vsize: 134236
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33352 0 0 0 54915 93 0 0 25 0 1 0 480389399 138506240 32597 4294967295 134512640 134672761 3221224528 3221223584 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33815 32597 603 41 0 33774 0
vsize: 135260
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33375 0 0 0 55916 93 0 0 25 0 1 0 480389399 137453568 32483 4294967295 134512640 134672761 3221224528 3221223712 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33558 32483 603 41 0 33517 0
vsize: 134232
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33375 0 0 0 56916 93 0 0 25 0 1 0 480389399 137453568 32483 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33558 32483 603 41 0 33517 0
vsize: 134232
[startup+580.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33375 0 0 0 57916 93 0 0 25 0 1 0 480389399 137453568 32483 4294967295 134512640 134672761 3221224528 3221223712 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33558 32483 603 41 0 33517 0
vsize: 134232
[startup+590.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33375 0 0 0 58916 93 0 0 25 0 1 0 480389399 137453568 32483 4294967295 134512640 134672761 3221224528 3221223712 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33558 32483 603 41 0 33517 0
vsize: 134232
[startup+600.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33375 0 0 0 59916 93 0 0 25 0 1 0 480389399 137453568 32483 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33558 32483 603 41 0 33517 0
vsize: 134232
[startup+610.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33376 0 0 0 60917 93 0 0 25 0 1 0 480389399 137453568 32484 4294967295 134512640 134672761 3221224528 3221223568 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33558 32484 603 41 0 33517 0
vsize: 134232
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33376 0 0 0 61917 93 0 0 25 0 1 0 480389399 137453568 32484 4294967295 134512640 134672761 3221224528 3221223712 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33558 32484 603 41 0 33517 0
vsize: 134232
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33376 0 0 0 62917 93 0 0 25 0 1 0 480389399 137453568 32484 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33558 32484 603 41 0 33517 0
vsize: 134232
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33376 0 0 0 63918 93 0 0 25 0 1 0 480389399 137453568 32484 4294967295 134512640 134672761 3221224528 3221223712 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33558 32484 603 41 0 33517 0
vsize: 134232
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33376 0 0 0 64918 93 0 0 25 0 1 0 480389399 137453568 32484 4294967295 134512640 134672761 3221224528 3221223712 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33558 32484 603 41 0 33517 0
vsize: 134232
[startup+660.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33376 0 0 0 65918 93 0 0 25 0 1 0 480389399 137453568 32484 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33558 32484 603 41 0 33517 0
vsize: 134232
[startup+670.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33376 0 0 0 66918 93 0 0 25 0 1 0 480389399 137453568 32484 4294967295 134512640 134672761 3221224528 3221223568 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33558 32484 603 41 0 33517 0
vsize: 134232
[startup+680.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33376 0 0 0 67918 93 0 0 25 0 1 0 480389399 137453568 32484 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33558 32484 603 41 0 33517 0
vsize: 134232
[startup+690.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33376 0 0 0 68919 93 0 0 25 0 1 0 480389399 137453568 32484 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33558 32484 603 41 0 33517 0
vsize: 134232
[startup+700.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33376 0 0 0 69919 93 0 0 25 0 1 0 480389399 137453568 32484 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33558 32484 603 41 0 33517 0
vsize: 134232
[startup+710.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33376 0 0 0 70919 93 0 0 25 0 1 0 480389399 137453568 32484 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33558 32484 603 41 0 33517 0
vsize: 134232
[startup+720.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33377 0 0 0 71919 93 0 0 25 0 1 0 480389399 137453568 32485 4294967295 134512640 134672761 3221224528 3221223712 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33558 32485 603 41 0 33517 0
vsize: 134232
[startup+730.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33377 0 0 0 72920 93 0 0 25 0 1 0 480389399 137453568 32485 4294967295 134512640 134672761 3221224528 3221223652 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33558 32485 603 41 0 33517 0
vsize: 134232
[startup+740.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33377 0 0 0 73920 93 0 0 25 0 1 0 480389399 137453568 32485 4294967295 134512640 134672761 3221224528 3221223712 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33558 32485 603 41 0 33517 0
vsize: 134232
[startup+750.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33377 0 0 0 74920 93 0 0 25 0 1 0 480389399 137453568 32485 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33558 32485 603 41 0 33517 0
vsize: 134232
[startup+760.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33377 0 0 0 75920 93 0 0 25 0 1 0 480389399 137453568 32485 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33558 32485 603 41 0 33517 0
vsize: 134232
[startup+770.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28691
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 33911 0 0 0 76919 94 0 0 25 0 1 0 480389399 139698176 33019 4294967295 134512640 134672761 3221224528 3221223712 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34106 33019 603 41 0 34065 0
vsize: 136424
[startup+780.023 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 28744
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 34601 0 0 0 77915 98 0 0 25 0 1 0 480389399 142602240 33709 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34815 33709 603 41 0 34774 0
vsize: 139260
[startup+790.023 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 28744
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 35152 0 0 0 78914 99 0 0 25 0 1 0 480389399 144850944 34260 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35364 34260 603 41 0 35323 0
vsize: 141456
[startup+800.023 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 28744
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 35664 0 0 0 79912 101 0 0 25 0 1 0 480389399 146972672 34772 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35882 34772 603 41 0 35841 0
vsize: 143528
[startup+810.024 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 28744
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 36102 0 0 0 80910 103 0 0 25 0 1 0 480389399 148676608 35210 4294967295 134512640 134672761 3221224528 3221223768 134615417 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36298 35210 603 41 0 36257 0
vsize: 145192
[startup+820.024 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 28744
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 36735 0 0 0 81910 104 0 0 25 0 1 0 480389399 151306240 35843 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36940 35843 603 41 0 36899 0
vsize: 147760
[startup+830.024 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28744
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 37426 0 0 0 82908 106 0 0 25 0 1 0 480389399 154206208 36534 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37648 36534 603 41 0 37607 0
vsize: 150592
[startup+840.025 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28744
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 38150 0 0 0 83907 108 0 0 25 0 1 0 480389399 157114368 37258 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38358 37258 603 41 0 38317 0
vsize: 153432
[startup+850.025 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 38812 0 0 0 84906 109 0 0 25 0 1 0 480389399 159920128 37920 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39043 37920 603 41 0 39002 0
vsize: 156172
[startup+860.025 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 39367 0 0 0 85904 110 0 0 25 0 1 0 480389399 162156544 38475 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39589 38475 603 41 0 39548 0
vsize: 158356
[startup+870.026 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 39846 0 0 0 86903 112 0 0 25 0 1 0 480389399 164126720 38954 4294967295 134512640 134672761 3221224528 3221223712 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40070 38954 603 41 0 40029 0
vsize: 160280
[startup+880.026 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 40421 0 0 0 87901 114 0 0 25 0 1 0 480389399 166473728 39529 4294967295 134512640 134672761 3221224528 3221223568 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40643 39529 603 41 0 40602 0
vsize: 162572
[startup+890.026 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 40931 0 0 0 88900 115 0 0 25 0 1 0 480389399 168574976 40039 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41156 40039 603 41 0 41115 0
vsize: 164624
[startup+900.027 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 41388 0 0 0 89899 116 0 0 25 0 1 0 480389399 170422272 40496 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41607 40496 603 41 0 41566 0
vsize: 166428
[startup+910.028 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 41832 0 0 0 90898 118 0 0 25 0 1 0 480389399 172363776 40940 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42081 40940 603 41 0 42040 0
vsize: 168324
[startup+920.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 42287 0 0 0 91897 119 0 0 25 0 1 0 480389399 174202880 41395 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42530 41395 603 41 0 42489 0
vsize: 170120
[startup+930.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 42791 0 0 0 92896 120 0 0 25 0 1 0 480389399 176439296 41899 4294967295 134512640 134672761 3221224528 3221223712 134615734 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43076 41899 603 41 0 43035 0
vsize: 172304
[startup+940.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 43333 0 0 0 93894 122 0 0 25 0 1 0 480389399 178532352 42441 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43587 42441 603 41 0 43546 0
vsize: 174348
[startup+950.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 43843 0 0 0 94893 123 0 0 25 0 1 0 480389399 180637696 42951 4294967295 134512640 134672761 3221224528 3221223712 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44101 42951 603 41 0 44060 0
vsize: 176404
[startup+960.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44496 0 0 0 95891 125 0 0 25 0 1 0 480389399 183541760 43572 4294967295 134512640 134672761 3221224528 3221223584 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44810 43572 603 41 0 44769 0
vsize: 179240
[startup+970.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44496 0 0 0 96891 125 0 0 25 0 1 0 480389399 183541760 43572 4294967295 134512640 134672761 3221224528 3221223584 134644269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44810 43572 603 41 0 44769 0
vsize: 179240
[startup+980.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44509 0 0 0 97892 125 0 0 25 0 1 0 480389399 183017472 43435 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44682 43435 603 41 0 44641 0
vsize: 178728
[startup+990.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44509 0 0 0 98892 125 0 0 25 0 1 0 480389399 183017472 43435 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44682 43435 603 41 0 44641 0
vsize: 178728
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44509 0 0 0 99892 125 0 0 25 0 1 0 480389399 183017472 43435 4294967295 134512640 134672761 3221224528 3221223712 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44682 43435 603 41 0 44641 0
vsize: 178728
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44509 0 0 0 100892 125 0 0 25 0 1 0 480389399 183017472 43435 4294967295 134512640 134672761 3221224528 3221223652 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44682 43435 603 41 0 44641 0
vsize: 178728
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44509 0 0 0 101892 126 0 0 25 0 1 0 480389399 183017472 43435 4294967295 134512640 134672761 3221224528 3221223712 134615638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44682 43435 603 41 0 44641 0
vsize: 178728
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44511 0 0 0 102892 126 0 0 25 0 1 0 480389399 183017472 43437 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44682 43437 603 41 0 44641 0
vsize: 178728
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44514 0 0 0 103892 126 0 0 25 0 1 0 480389399 183017472 43440 4294967295 134512640 134672761 3221224528 3221223712 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44682 43440 603 41 0 44641 0
vsize: 178728
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44519 0 0 0 104892 126 0 0 25 0 1 0 480389399 183017472 43445 4294967295 134512640 134672761 3221224528 3221223728 134610709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44682 43445 603 41 0 44641 0
vsize: 178728
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44520 0 0 0 105893 126 0 0 25 0 1 0 480389399 183017472 43446 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44682 43446 603 41 0 44641 0
vsize: 178728
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44520 0 0 0 106893 126 0 0 25 0 1 0 480389399 183017472 43446 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44682 43446 603 41 0 44641 0
vsize: 178728
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44522 0 0 0 107893 126 0 0 25 0 1 0 480389399 183017472 43448 4294967295 134512640 134672761 3221224528 3221223712 134615635 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44682 43448 603 41 0 44641 0
vsize: 178728
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44523 0 0 0 108893 126 0 0 25 0 1 0 480389399 183017472 43449 4294967295 134512640 134672761 3221224528 3221223712 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44682 43449 603 41 0 44641 0
vsize: 178728
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44524 0 0 0 109893 126 0 0 25 0 1 0 480389399 183017472 43450 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44682 43450 603 41 0 44641 0
vsize: 178728
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28746
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44524 0 0 0 110893 126 0 0 25 0 1 0 480389399 183017472 43450 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44682 43450 603 41 0 44641 0
vsize: 178728
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28748
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44524 0 0 0 111893 126 0 0 25 0 1 0 480389399 183017472 43450 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44682 43450 603 41 0 44641 0
vsize: 178728
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28748
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44524 0 0 0 112894 126 0 0 25 0 1 0 480389399 183017472 43450 4294967295 134512640 134672761 3221224528 3221223568 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44682 43450 603 41 0 44641 0
vsize: 178728
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28748
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44524 0 0 0 113894 126 0 0 25 0 1 0 480389399 183017472 43450 4294967295 134512640 134672761 3221224528 3221223712 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44682 43450 603 41 0 44641 0
vsize: 178728
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28748
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44524 0 0 0 114894 126 0 0 25 0 1 0 480389399 183017472 43450 4294967295 134512640 134672761 3221224528 3221223712 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44682 43450 603 41 0 44641 0
vsize: 178728
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28748
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44525 0 0 0 115894 126 0 0 25 0 1 0 480389399 183017472 43451 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44682 43451 603 41 0 44641 0
vsize: 178728
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28748
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44525 0 0 0 116894 126 0 0 25 0 1 0 480389399 183017472 43451 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44682 43451 603 41 0 44641 0
vsize: 178728
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28748
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44525 0 0 0 117894 126 0 0 25 0 1 0 480389399 183017472 43451 4294967295 134512640 134672761 3221224528 3221223712 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44682 43451 603 41 0 44641 0
vsize: 178728
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28748
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44525 0 0 0 118895 126 0 0 25 0 1 0 480389399 183017472 43451 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44682 43451 603 41 0 44641 0
vsize: 178728
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28748
Raw data (stat): 28691 (minisat+) R 28690 22612 22611 0 -1 0 44525 0 0 0 119895 126 0 0 25 0 1 0 480389399 183017472 43451 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44682 43451 603 41 0 44641 0
vsize: 178728
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 28748
Raw data (stat): 28691 (minisat+) Z 28690 22612 22611 0 -1 12 44525 0 0 0 119895 135 0 0 25 0 1 0 480389399 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.12
CPU time (s): 1200.31
CPU user time (s): 1198.95
CPU system time (s): 1.35279
CPU usage (%): 100.016
Max. virtual memory (Kb): 179240
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####