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 6358

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        830744 kB
Buffers:         41292 kB
Cached:         137820 kB
SwapCached:          0 kB
Active:         112952 kB
Inactive:        69304 kB
HighTotal:      131008 kB
HighFree:          588 kB
LowTotal:       903652 kB
LowFree:        830156 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           7200 kB
Slab:            15920 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:51:33 (client local time) WITH STATUS 0 IN 1200.28 SECONDS
stats: 4811 7 1200.28 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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  122857   308719 |   40952       0        0     nan |  0.000 % |
c |       100 |  122857   308719 |   45047     100     1187    11.9 |  7.945 % |
c |       252 |  122857   308719 |   49551     252     3497    13.9 |  7.945 % |
c |       477 |  122857   308719 |   54507     477     8197    17.2 |  7.945 % |
c |       815 |  122857   308719 |   59957     815    30150    37.0 |  7.945 % |
c |      1321 |  122857   308719 |   65953    1321    48418    36.7 |  7.945 % |
c |      2081 |  122857   308719 |   72548    2081    61230    29.4 |  7.945 % |
c |      3220 |  122851   308706 |   79803    3219    85430    26.5 |  7.950 % |
c |      4928 |  122840   308682 |   87784    4926   309185    62.8 |  7.958 % |
c |      7490 |  122840   308682 |   96562    7488   425884    56.9 |  7.958 % |
c |     11334 |  122840   308682 |  106218   11332   764166    67.4 |  7.958 % |
c |     17100 |  122840   308682 |  116840   17098   919040    53.8 |  7.958 % |
c |     25750 |  122840   308682 |  128524   25748  2236843    86.9 |  7.958 % |
c |     38724 |  122840   308682 |  141377   38722  3509561    90.6 |  7.958 % |
c |     58186 |  122840   308682 |  155515   58184  6139854   105.5 |  7.958 % |
c |     87378 |  122837   308676 |  171066   87375  8323023    95.3 |  7.960 % |
c |    131167 |  122837   308676 |  188173  131164 11810504    90.0 |  7.960 % |
c |    196852 |  115145   291148 |  206990  196299 15586994    79.4 | 13.217 % |
c |    295379 |  107233   272852 |  227689   94985  7551046    79.5 | 19.268 % |
#### 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.67 0.90 0.94 2/56 22430
Raw data (stat): 22430 (runsolver) R 22429 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 366654802 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.72 0.90 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 5577 0 0 0 985 13 0 0 25 0 1 0 366654802 24961024 5349 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6094 5349 603 41 0 6053 0
vsize: 24376
[startup+20.0008 s]
Raw data (loadavg): 0.76 0.90 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 5585 0 0 0 1985 13 0 0 25 0 1 0 366654802 24961024 5357 4294967295 134512640 134672761 3221224528 3221223696 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6094 5357 603 41 0 6053 0
vsize: 24376
[startup+30.0016 s]
Raw data (loadavg): 0.80 0.91 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 5585 0 0 0 2985 14 0 0 25 0 1 0 366654802 24961024 5357 4294967295 134512640 134672761 3221224528 3221223692 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6094 5357 603 41 0 6053 0
vsize: 24376
[startup+40.0014 s]
Raw data (loadavg): 0.83 0.91 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 5840 0 0 0 3984 15 0 0 25 0 1 0 366654802 25894912 5612 4294967295 134512640 134672761 3221224528 3221223632 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6322 5612 603 41 0 6281 0
vsize: 25288
[startup+50.0027 s]
Raw data (loadavg): 0.85 0.91 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 6454 0 0 0 4983 16 0 0 25 0 1 0 366654802 28434432 6226 4294967295 134512640 134672761 3221224528 3221223664 134560625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6942 6226 603 41 0 6901 0
vsize: 27768
[startup+60.002 s]
Raw data (loadavg): 0.88 0.91 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 7005 0 0 0 5981 18 0 0 25 0 1 0 366654802 30695424 6777 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7494 6777 603 41 0 7453 0
vsize: 29976
[startup+70.0028 s]
Raw data (loadavg): 0.89 0.92 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 7467 0 0 0 6979 20 0 0 25 0 1 0 366654802 32567296 7239 4294967295 134512640 134672761 3221224528 3221223696 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7951 7239 603 41 0 7910 0
vsize: 31804
[startup+80.0036 s]
Raw data (loadavg): 0.91 0.92 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 7796 0 0 0 7978 21 0 0 25 0 1 0 366654802 34033664 7568 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8309 7568 603 41 0 8268 0
vsize: 33236
[startup+90.0033 s]
Raw data (loadavg): 0.92 0.92 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 8214 0 0 0 8976 23 0 0 25 0 1 0 366654802 35774464 7986 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8734 7986 603 41 0 8693 0
vsize: 34936
[startup+100.003 s]
Raw data (loadavg): 0.93 0.92 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 8589 0 0 0 9974 25 0 0 25 0 1 0 366654802 37236736 8361 4294967295 134512640 134672761 3221224528 3221223684 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9091 8361 603 41 0 9050 0
vsize: 36364
[startup+110.003 s]
Raw data (loadavg): 0.94 0.92 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 8955 0 0 0 10972 27 0 0 25 0 1 0 366654802 38711296 8727 4294967295 134512640 134672761 3221224528 3221223664 134565064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9451 8727 603 41 0 9410 0
vsize: 37804
[startup+120.005 s]
Raw data (loadavg): 0.95 0.93 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 9427 0 0 0 11971 29 0 0 25 0 1 0 366654802 40706048 9199 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9938 9199 603 41 0 9897 0
vsize: 39752
[startup+130.004 s]
Raw data (loadavg): 0.96 0.93 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 9965 0 0 0 12969 30 0 0 25 0 1 0 366654802 42835968 9737 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10458 9737 603 41 0 10417 0
vsize: 41832
[startup+140.004 s]
Raw data (loadavg): 0.97 0.93 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 10446 0 0 0 13968 32 0 0 25 0 1 0 366654802 44855296 10218 4294967295 134512640 134672761 3221224528 3221223712 134558557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10951 10218 603 41 0 10910 0
vsize: 43804
[startup+150.005 s]
Raw data (loadavg): 0.97 0.93 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 10841 0 0 0 14967 33 0 0 25 0 1 0 366654802 46460928 10613 4294967295 134512640 134672761 3221224528 3221223696 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11343 10613 603 41 0 11302 0
vsize: 45372
[startup+160.005 s]
Raw data (loadavg): 0.97 0.93 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 11101 0 0 0 15966 33 0 0 25 0 1 0 366654802 47529984 10873 4294967295 134512640 134672761 3221224528 3221223652 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11604 10873 603 41 0 11563 0
vsize: 46416
[startup+170.005 s]
Raw data (loadavg): 0.98 0.94 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 11457 0 0 0 16965 35 0 0 25 0 1 0 366654802 48984064 11229 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11959 11229 603 41 0 11918 0
vsize: 47836
[startup+180.005 s]
Raw data (loadavg): 0.98 0.94 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 11765 0 0 0 17964 36 0 0 25 0 1 0 366654802 50192384 11537 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12254 11537 603 41 0 12213 0
vsize: 49016
[startup+190.005 s]
Raw data (loadavg): 0.98 0.94 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 12056 0 0 0 18964 36 0 0 25 0 1 0 366654802 51646464 11828 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12609 11828 603 41 0 12568 0
vsize: 50436
[startup+200.005 s]
Raw data (loadavg): 0.98 0.94 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 12304 0 0 0 19963 37 0 0 25 0 1 0 366654802 52715520 12076 4294967295 134512640 134672761 3221224528 3221223632 134560396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 12076 603 41 0 12829 0
vsize: 51480
[startup+210.005 s]
Raw data (loadavg): 0.99 0.94 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 12502 0 0 0 20963 38 0 0 25 0 1 0 366654802 53534720 12274 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13070 12274 603 41 0 13029 0
vsize: 52280
[startup+220.006 s]
Raw data (loadavg): 0.99 0.94 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 12684 0 0 0 21962 39 0 0 25 0 1 0 366654802 54194176 12456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13231 12456 603 41 0 13190 0
vsize: 52924
[startup+230.006 s]
Raw data (loadavg): 0.99 0.94 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 12838 0 0 0 22962 39 0 0 25 0 1 0 366654802 54861824 12610 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13394 12610 603 41 0 13353 0
vsize: 53576
[startup+240.006 s]
Raw data (loadavg): 0.99 0.95 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 13032 0 0 0 23961 40 0 0 25 0 1 0 366654802 55664640 12804 4294967295 134512640 134672761 3221224528 3221223632 134560198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13590 12804 603 41 0 13549 0
vsize: 54360
[startup+250.006 s]
Raw data (loadavg): 0.99 0.95 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 13139 0 0 0 24962 40 0 0 25 0 1 0 366654802 56061952 12911 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13687 12911 603 41 0 13646 0
vsize: 54748
[startup+260.006 s]
Raw data (loadavg): 0.99 0.95 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 13404 0 0 0 25961 41 0 0 25 0 1 0 366654802 57180160 13176 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13960 13176 603 41 0 13919 0
vsize: 55840
[startup+270.007 s]
Raw data (loadavg): 0.99 0.95 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 13824 0 0 0 26960 42 0 0 25 0 1 0 366654802 58912768 13596 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14383 13596 603 41 0 14342 0
vsize: 57532
[startup+280.006 s]
Raw data (loadavg): 0.99 0.95 0.94 2/56 22430
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 14436 0 0 0 27958 44 0 0 25 0 1 0 366654802 61333504 14208 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14974 14208 603 41 0 14933 0
vsize: 59896
[startup+290.007 s]
Raw data (loadavg): 0.99 0.95 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 14793 0 0 0 28956 45 0 0 25 0 1 0 366654802 62795776 14565 4294967295 134512640 134672761 3221224528 3221223632 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15331 14565 603 41 0 15290 0
vsize: 61324
[startup+300.007 s]
Raw data (loadavg): 0.99 0.95 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 14960 0 0 0 29956 46 0 0 25 0 1 0 366654802 63467520 14732 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15495 14732 603 41 0 15454 0
vsize: 61980
[startup+310.007 s]
Raw data (loadavg): 0.99 0.95 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 15192 0 0 0 30955 47 0 0 25 0 1 0 366654802 64532480 14964 4294967295 134512640 134672761 3221224528 3221223696 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15755 14964 603 41 0 15714 0
vsize: 63020
[startup+320.007 s]
Raw data (loadavg): 0.99 0.95 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 15424 0 0 0 31954 48 0 0 25 0 1 0 366654802 65458176 15196 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15981 15196 603 41 0 15940 0
vsize: 63924
[startup+330.008 s]
Raw data (loadavg): 0.99 0.95 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 15641 0 0 0 32954 49 0 0 25 0 1 0 366654802 66387968 15413 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16208 15413 603 41 0 16167 0
vsize: 64832
[startup+340.008 s]
Raw data (loadavg): 0.99 0.96 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 15846 0 0 0 33953 49 0 0 25 0 1 0 366654802 67186688 15618 4294967295 134512640 134672761 3221224528 3221223728 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16403 15618 603 41 0 16362 0
vsize: 65612
[startup+350.008 s]
Raw data (loadavg): 0.99 0.96 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 16005 0 0 0 34953 50 0 0 25 0 1 0 366654802 67858432 15777 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16567 15777 603 41 0 16526 0
vsize: 66268
[startup+360.009 s]
Raw data (loadavg): 0.99 0.96 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 16171 0 0 0 35952 51 0 0 25 0 1 0 366654802 68517888 15943 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16728 15943 603 41 0 16687 0
vsize: 66912
[startup+370.009 s]
Raw data (loadavg): 0.99 0.96 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 16351 0 0 0 36951 52 0 0 25 0 1 0 366654802 69185536 16123 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16891 16123 603 41 0 16850 0
vsize: 67564
[startup+380.009 s]
Raw data (loadavg): 0.99 0.96 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 16525 0 0 0 37950 53 0 0 25 0 1 0 366654802 69844992 16297 4294967295 134512640 134672761 3221224528 3221223632 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17052 16298 603 41 0 17011 0
vsize: 68208
[startup+390.009 s]
Raw data (loadavg): 0.99 0.96 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 16679 0 0 0 38950 54 0 0 25 0 1 0 366654802 70508544 16451 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17214 16451 603 41 0 17173 0
vsize: 68856
[startup+400.01 s]
Raw data (loadavg): 0.99 0.96 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 16837 0 0 0 39949 54 0 0 25 0 1 0 366654802 71172096 16609 4294967295 134512640 134672761 3221224528 3221223696 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17376 16609 603 41 0 17335 0
vsize: 69504
[startup+410.01 s]
Raw data (loadavg): 0.99 0.96 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 16997 0 0 0 40949 55 0 0 25 0 1 0 366654802 71839744 16769 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17539 16769 603 41 0 17498 0
vsize: 70156
[startup+420.01 s]
Raw data (loadavg): 0.99 0.96 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 17135 0 0 0 41949 55 0 0 25 0 1 0 366654802 72376320 16907 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17670 16907 603 41 0 17629 0
vsize: 70680
[startup+430.01 s]
Raw data (loadavg): 0.99 0.96 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 17281 0 0 0 42949 55 0 0 25 0 1 0 366654802 72912896 17053 4294967295 134512640 134672761 3221224528 3221223712 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17801 17053 603 41 0 17760 0
vsize: 71204
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 17415 0 0 0 43949 56 0 0 25 0 1 0 366654802 73998336 17187 4294967295 134512640 134672761 3221224528 3221223632 134560201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18066 17187 603 41 0 18025 0
vsize: 72264
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 17549 0 0 0 44948 56 0 0 25 0 1 0 366654802 74522624 17321 4294967295 134512640 134672761 3221224528 3221223632 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18194 17321 603 41 0 18153 0
vsize: 72776
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 17680 0 0 0 45948 57 0 0 25 0 1 0 366654802 75051008 17452 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18323 17452 603 41 0 18282 0
vsize: 73292
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 17801 0 0 0 46948 57 0 0 25 0 1 0 366654802 75579392 17573 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18452 17573 603 41 0 18411 0
vsize: 73808
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 17906 0 0 0 47947 58 0 0 25 0 1 0 366654802 75976704 17678 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18549 17678 603 41 0 18508 0
vsize: 74196
[startup+490.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 18023 0 0 0 48947 58 0 0 25 0 1 0 366654802 76509184 17795 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18679 17795 603 41 0 18638 0
vsize: 74716
[startup+500.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 18136 0 0 0 49946 59 0 0 25 0 1 0 366654802 76902400 17908 4294967295 134512640 134672761 3221224528 3221223632 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18775 17908 603 41 0 18734 0
vsize: 75100
[startup+510.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 18237 0 0 0 50946 60 0 0 25 0 1 0 366654802 77295616 18009 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18871 18009 603 41 0 18830 0
vsize: 75484
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 18386 0 0 0 51946 60 0 0 25 0 1 0 366654802 77897728 18158 4294967295 134512640 134672761 3221224528 3221223728 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19018 18158 603 41 0 18977 0
vsize: 76072
[startup+530.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 18526 0 0 0 52946 60 0 0 25 0 1 0 366654802 78708736 18298 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19216 18298 603 41 0 19175 0
vsize: 76864
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 18675 0 0 0 53945 61 0 0 25 0 1 0 366654802 79368192 18447 4294967295 134512640 134672761 3221224528 3221223696 134561256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19377 18447 603 41 0 19336 0
vsize: 77508
[startup+550.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 18824 0 0 0 54945 62 0 0 25 0 1 0 366654802 79892480 18596 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19505 18596 603 41 0 19464 0
vsize: 78020
[startup+560.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 18965 0 0 0 55944 62 0 0 25 0 1 0 366654802 80551936 18737 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19666 18737 603 41 0 19625 0
vsize: 78664
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 19090 0 0 0 56944 62 0 0 25 0 1 0 366654802 80957440 18862 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19765 18862 603 41 0 19724 0
vsize: 79060
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22432
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 19226 0 0 0 57944 63 0 0 25 0 1 0 366654802 81494016 18998 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19896 18998 603 41 0 19855 0
vsize: 79584
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 19681 0 0 0 58943 63 0 0 25 0 1 0 366654802 83484672 19453 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20382 19453 603 41 0 20341 0
vsize: 81528
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 20044 0 0 0 59943 64 0 0 25 0 1 0 366654802 84951040 19816 4294967295 134512640 134672761 3221224528 3221223696 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20740 19816 603 41 0 20699 0
vsize: 82960
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 20191 0 0 0 60942 65 0 0 25 0 1 0 366654802 85483520 19963 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20870 19963 603 41 0 20829 0
vsize: 83480
[startup+620.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 20300 0 0 0 61942 65 0 0 25 0 1 0 366654802 85880832 20072 4294967295 134512640 134672761 3221224528 3221223632 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20967 20072 603 41 0 20926 0
vsize: 83868
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 20460 0 0 0 62942 66 0 0 25 0 1 0 366654802 86806528 20232 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21193 20232 603 41 0 21152 0
vsize: 84772
[startup+640.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 20618 0 0 0 63942 66 0 0 25 0 1 0 366654802 87339008 20390 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21323 20390 603 41 0 21282 0
vsize: 85292
[startup+650.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 20802 0 0 0 64941 66 0 0 25 0 1 0 366654802 88145920 20574 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21520 20574 603 41 0 21479 0
vsize: 86080
[startup+660.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 20954 0 0 0 65941 67 0 0 25 0 1 0 366654802 88678400 20726 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21650 20726 603 41 0 21609 0
vsize: 86600
[startup+670.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 21099 0 0 0 66941 67 0 0 25 0 1 0 366654802 89333760 20871 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21810 20871 603 41 0 21769 0
vsize: 87240
[startup+680.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 21266 0 0 0 67940 68 0 0 25 0 1 0 366654802 89997312 21038 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21972 21038 603 41 0 21931 0
vsize: 87888
[startup+690.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 21405 0 0 0 68940 69 0 0 25 0 1 0 366654802 90529792 21177 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22102 21177 603 41 0 22061 0
vsize: 88408
[startup+700.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 21547 0 0 0 69940 69 0 0 25 0 1 0 366654802 91054080 21319 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22230 21319 603 41 0 22189 0
vsize: 88920
[startup+710.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 21675 0 0 0 70939 70 0 0 25 0 1 0 366654802 91582464 21447 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22359 21447 603 41 0 22318 0
vsize: 89436
[startup+720.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 21798 0 0 0 71939 70 0 0 25 0 1 0 366654802 92114944 21570 4294967295 134512640 134672761 3221224528 3221223584 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22489 21570 603 41 0 22448 0
vsize: 89956
[startup+730.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 21906 0 0 0 72938 71 0 0 25 0 1 0 366654802 92512256 21678 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22586 21678 603 41 0 22545 0
vsize: 90344
[startup+740.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 21976 0 0 0 73938 71 0 0 25 0 1 0 366654802 92774400 21748 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22650 21748 603 41 0 22609 0
vsize: 90600
[startup+750.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 22047 0 0 0 74938 72 0 0 25 0 1 0 366654802 93036544 21819 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22714 21819 603 41 0 22673 0
vsize: 90856
[startup+760.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 22208 0 0 0 75937 72 0 0 25 0 1 0 366654802 93708288 21980 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22878 21980 603 41 0 22837 0
vsize: 91512
[startup+770.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 22453 0 0 0 76937 72 0 0 25 0 1 0 366654802 94904320 22225 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23170 22225 603 41 0 23129 0
vsize: 92680
[startup+780.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 22659 0 0 0 77936 73 0 0 25 0 1 0 366654802 95739904 22431 4294967295 134512640 134672761 3221224528 3221223712 134558654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23374 22431 603 41 0 23333 0
vsize: 93496
[startup+790.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 22838 0 0 0 78936 74 0 0 25 0 1 0 366654802 96534528 22610 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23568 22610 603 41 0 23527 0
vsize: 94272
[startup+800.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 22980 0 0 0 79936 74 0 0 25 0 1 0 366654802 97062912 22752 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23697 22752 603 41 0 23656 0
vsize: 94788
[startup+810.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23120 0 0 0 80935 75 0 0 25 0 1 0 366654802 97591296 22892 4294967295 134512640 134672761 3221224528 3221223696 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23826 22892 603 41 0 23785 0
vsize: 95304
[startup+820.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23267 0 0 0 81935 75 0 0 25 0 1 0 366654802 98267136 23039 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23991 23039 603 41 0 23950 0
vsize: 95964
[startup+830.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23342 0 0 0 82935 75 0 0 25 0 1 0 366654802 98529280 23114 4294967295 134512640 134672761 3221224528 3221223632 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23114 603 41 0 24014 0
vsize: 96220
[startup+840.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23342 0 0 0 83935 75 0 0 25 0 1 0 366654802 98529280 23114 4294967295 134512640 134672761 3221224528 3221223632 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23114 603 41 0 24014 0
vsize: 96220
[startup+850.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23342 0 0 0 84935 75 0 0 25 0 1 0 366654802 98529280 23114 4294967295 134512640 134672761 3221224528 3221223632 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23114 603 41 0 24014 0
vsize: 96220
[startup+860.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23342 0 0 0 85936 75 0 0 25 0 1 0 366654802 98529280 23114 4294967295 134512640 134672761 3221224528 3221223632 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23114 603 41 0 24014 0
vsize: 96220
[startup+870.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23342 0 0 0 86936 75 0 0 25 0 1 0 366654802 98529280 23114 4294967295 134512640 134672761 3221224528 3221223632 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23114 603 41 0 24014 0
vsize: 96220
[startup+880.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22434
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23342 0 0 0 87936 75 0 0 25 0 1 0 366654802 98529280 23114 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23114 603 41 0 24014 0
vsize: 96220
[startup+890.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23342 0 0 0 88936 75 0 0 25 0 1 0 366654802 98529280 23114 4294967295 134512640 134672761 3221224528 3221223728 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23114 603 41 0 24014 0
vsize: 96220
[startup+900.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23342 0 0 0 89936 75 0 0 25 0 1 0 366654802 98529280 23114 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23114 603 41 0 24014 0
vsize: 96220
[startup+910.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23342 0 0 0 90936 75 0 0 25 0 1 0 366654802 98529280 23114 4294967295 134512640 134672761 3221224528 3221223632 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23114 603 41 0 24014 0
vsize: 96220
[startup+920.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23342 0 0 0 91937 75 0 0 25 0 1 0 366654802 98529280 23114 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23114 603 41 0 24014 0
vsize: 96220
[startup+930.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23344 0 0 0 92937 75 0 0 25 0 1 0 366654802 98529280 23116 4294967295 134512640 134672761 3221224528 3221223632 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23116 603 41 0 24014 0
vsize: 96220
[startup+940.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23344 0 0 0 93937 75 0 0 25 0 1 0 366654802 98529280 23116 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23116 603 41 0 24014 0
vsize: 96220
[startup+950.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23344 0 0 0 94937 75 0 0 25 0 1 0 366654802 98529280 23116 4294967295 134512640 134672761 3221224528 3221223696 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23116 603 41 0 24014 0
vsize: 96220
[startup+960.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23345 0 0 0 95937 75 0 0 25 0 1 0 366654802 98529280 23117 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23117 603 41 0 24014 0
vsize: 96220
[startup+970.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 96938 75 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223696 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
[startup+980.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 97938 75 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
[startup+990.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 98938 75 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 99938 75 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223664 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 100938 75 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 101938 75 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 102939 75 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 103939 75 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223712 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 104939 75 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223672 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 105939 75 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223632 134555373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 106939 75 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 107939 75 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 108940 75 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 109940 75 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 110940 75 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 111940 75 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 112946 75 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 113946 76 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223696 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 114947 76 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 115947 76 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223600 134553549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 116947 76 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22436
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 117947 76 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223632 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22438
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 118947 76 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 22438
Raw data (stat): 22430 (minisat+) R 22429 12452 12451 0 -1 0 23346 0 0 0 119947 76 0 0 25 0 1 0 366654802 98529280 23118 4294967295 134512640 134672761 3221224528 3221223696 134560976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24055 23118 603 41 0 24014 0
vsize: 96220
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.94 1/56 22438
Raw data (stat): 22430 (minisat+) Z 22429 12452 12451 0 -1 12 23348 0 0 0 119947 80 0 0 25 0 1 0 366654802 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.28
CPU user time (s): 1199.47
CPU system time (s): 0.807877
CPU usage (%): 100.013
Max. virtual memory (Kb): 96220
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####