YES(?, 2*a^2 + 8*a + c + 12)

Initial complexity problem:
1:	T:
		(?, 1)    start(a, b, c, d, e, f) -> stop(a, b, c, f, e, f) [ 0 >= a /\ b = c /\ d = e /\ f = a ]
		(?, 1)    start(a, b, c, d, e, f) -> lbl52(a, b - 1, c, f, e, f) [ a >= 1 /\ c >= 1 /\ b = c /\ d = e /\ f = a ]
		(?, 1)    start(a, b, c, d, e, f) -> lbl72(a, f, c, f - 1, e, f) [ a >= 1 /\ 0 >= c /\ b = c /\ d = e /\ f = a ]
		(?, 1)    lbl52(a, b, c, d, e, f) -> stop(a, b, c, d, e, f) [ 0 >= d /\ b >= 0 /\ d >= 1 /\ a >= d /\ f = a ]
		(?, 1)    lbl52(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\ b >= 1 /\ b >= 0 /\ a >= d /\ f = a ]
		(?, 1)    lbl52(a, b, c, d, e, f) -> lbl72(a, f, c, d - 1, e, f) [ d >= 1 /\ a >= d /\ b = 0 /\ f = a ]
		(?, 1)    lbl72(a, b, c, d, e, f) -> stop(a, b, c, d, e, f) [ a >= 1 /\ d = 0 /\ f = a /\ b = a ]
		(?, 1)    lbl72(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\ a >= 1 /\ d >= 0 /\ a >= d + 1 /\ f = a /\ b = a ]
		(?, 1)    lbl72(a, b, c, d, e, f) -> lbl72(a, f, c, d - 1, e, f) [ d >= 1 /\ 0 >= a /\ d >= 0 /\ a >= d + 1 /\ f = a /\ b = a ]
		(1, 1)    start0(a, b, c, d, e, f) -> start(a, c, c, e, e, a)
	start location:	start0
	leaf cost:	0

Testing for unsatisfiable constraints removes the following transitions from problem 1:
	lbl52(a, b, c, d, e, f) -> stop(a, b, c, d, e, f) [ 0 >= d /\ b >= 0 /\ d >= 1 /\ a >= d /\ f = a ]
	lbl72(a, b, c, d, e, f) -> lbl72(a, f, c, d - 1, e, f) [ d >= 1 /\ 0 >= a /\ d >= 0 /\ a >= d + 1 /\ f = a /\ b = a ]
We thus obtain the following problem:
2:	T:
		(?, 1)    start(a, b, c, d, e, f) -> stop(a, b, c, f, e, f) [ 0 >= a /\ b = c /\ d = e /\ f = a ]
		(?, 1)    start(a, b, c, d, e, f) -> lbl52(a, b - 1, c, f, e, f) [ a >= 1 /\ c >= 1 /\ b = c /\ d = e /\ f = a ]
		(?, 1)    start(a, b, c, d, e, f) -> lbl72(a, f, c, f - 1, e, f) [ a >= 1 /\ 0 >= c /\ b = c /\ d = e /\ f = a ]
		(?, 1)    lbl52(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\ b >= 1 /\ b >= 0 /\ a >= d /\ f = a ]
		(?, 1)    lbl52(a, b, c, d, e, f) -> lbl72(a, f, c, d - 1, e, f) [ d >= 1 /\ a >= d /\ b = 0 /\ f = a ]
		(?, 1)    lbl72(a, b, c, d, e, f) -> stop(a, b, c, d, e, f) [ a >= 1 /\ d = 0 /\ f = a /\ b = a ]
		(?, 1)    lbl72(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\ a >= 1 /\ d >= 0 /\ a >= d + 1 /\ f = a /\ b = a ]
		(1, 1)    start0(a, b, c, d, e, f) -> start(a, c, c, e, e, a)
	start location:	start0
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem:
3:	T:
		(?, 1)    start(a, b, c, d, e, f) -> lbl52(a, b - 1, c, f, e, f) [ a >= 1 /\ c >= 1 /\ b = c /\ d = e /\ f = a ]
		(?, 1)    start(a, b, c, d, e, f) -> lbl72(a, f, c, f - 1, e, f) [ a >= 1 /\ 0 >= c /\ b = c /\ d = e /\ f = a ]
		(?, 1)    lbl52(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\ b >= 1 /\ b >= 0 /\ a >= d /\ f = a ]
		(?, 1)    lbl52(a, b, c, d, e, f) -> lbl72(a, f, c, d - 1, e, f) [ d >= 1 /\ a >= d /\ b = 0 /\ f = a ]
		(?, 1)    lbl72(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\ a >= 1 /\ d >= 0 /\ a >= d + 1 /\ f = a /\ b = a ]
		(1, 1)    start0(a, b, c, d, e, f) -> start(a, c, c, e, e, a)
	start location:	start0
	leaf cost:	2

Repeatedly propagating knowledge in problem 3 produces the following problem:
4:	T:
		(1, 1)    start(a, b, c, d, e, f) -> lbl52(a, b - 1, c, f, e, f) [ a >= 1 /\ c >= 1 /\ b = c /\ d = e /\ f = a ]
		(1, 1)    start(a, b, c, d, e, f) -> lbl72(a, f, c, f - 1, e, f) [ a >= 1 /\ 0 >= c /\ b = c /\ d = e /\ f = a ]
		(?, 1)    lbl52(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\ b >= 1 /\ b >= 0 /\ a >= d /\ f = a ]
		(?, 1)    lbl52(a, b, c, d, e, f) -> lbl72(a, f, c, d - 1, e, f) [ d >= 1 /\ a >= d /\ b = 0 /\ f = a ]
		(?, 1)    lbl72(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\ a >= 1 /\ d >= 0 /\ a >= d + 1 /\ f = a /\ b = a ]
		(1, 1)    start0(a, b, c, d, e, f) -> start(a, c, c, e, e, a)
	start location:	start0
	leaf cost:	2

A polynomial rank function with
	Pol(start) = 2*V_6 + 2
	Pol(lbl52) = 2*V_4 + 2
	Pol(lbl72) = 2*V_4 + 3
	Pol(start0) = 2*V_1 + 2
orients all transitions weakly and the transitions
	lbl72(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\ a >= 1 /\ d >= 0 /\ a >= d + 1 /\ f = a /\ b = a ]
	lbl52(a, b, c, d, e, f) -> lbl72(a, f, c, d - 1, e, f) [ d >= 1 /\ a >= d /\ b = 0 /\ f = a ]
strictly and produces the following problem:
5:	T:
		(1, 1)          start(a, b, c, d, e, f) -> lbl52(a, b - 1, c, f, e, f) [ a >= 1 /\ c >= 1 /\ b = c /\ d = e /\ f = a ]
		(1, 1)          start(a, b, c, d, e, f) -> lbl72(a, f, c, f - 1, e, f) [ a >= 1 /\ 0 >= c /\ b = c /\ d = e /\ f = a ]
		(?, 1)          lbl52(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\ b >= 1 /\ b >= 0 /\ a >= d /\ f = a ]
		(2*a + 2, 1)    lbl52(a, b, c, d, e, f) -> lbl72(a, f, c, d - 1, e, f) [ d >= 1 /\ a >= d /\ b = 0 /\ f = a ]
		(2*a + 2, 1)    lbl72(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\ a >= 1 /\ d >= 0 /\ a >= d + 1 /\ f = a /\ b = a ]
		(1, 1)          start0(a, b, c, d, e, f) -> start(a, c, c, e, e, a)
	start location:	start0
	leaf cost:	2

A polynomial rank function with
	Pol(lbl52) = V_2 + 1
and size complexities
	S("start0(a, b, c, d, e, f) -> start(a, c, c, e, e, a)", 0-0) = a
	S("start0(a, b, c, d, e, f) -> start(a, c, c, e, e, a)", 0-1) = c
	S("start0(a, b, c, d, e, f) -> start(a, c, c, e, e, a)", 0-2) = c
	S("start0(a, b, c, d, e, f) -> start(a, c, c, e, e, a)", 0-3) = e
	S("start0(a, b, c, d, e, f) -> start(a, c, c, e, e, a)", 0-4) = e
	S("start0(a, b, c, d, e, f) -> start(a, c, c, e, e, a)", 0-5) = a
	S("lbl72(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\\ a >= 1 /\\ d >= 0 /\\ a >= d + 1 /\\ f = a /\\ b = a ]", 0-0) = a
	S("lbl72(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\\ a >= 1 /\\ d >= 0 /\\ a >= d + 1 /\\ f = a /\\ b = a ]", 0-1) = a
	S("lbl72(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\\ a >= 1 /\\ d >= 0 /\\ a >= d + 1 /\\ f = a /\\ b = a ]", 0-2) = c
	S("lbl72(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\\ a >= 1 /\\ d >= 0 /\\ a >= d + 1 /\\ f = a /\\ b = a ]", 0-3) = a
	S("lbl72(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\\ a >= 1 /\\ d >= 0 /\\ a >= d + 1 /\\ f = a /\\ b = a ]", 0-4) = e
	S("lbl72(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\\ a >= 1 /\\ d >= 0 /\\ a >= d + 1 /\\ f = a /\\ b = a ]", 0-5) = a
	S("lbl52(a, b, c, d, e, f) -> lbl72(a, f, c, d - 1, e, f) [ d >= 1 /\\ a >= d /\\ b = 0 /\\ f = a ]", 0-0) = a
	S("lbl52(a, b, c, d, e, f) -> lbl72(a, f, c, d - 1, e, f) [ d >= 1 /\\ a >= d /\\ b = 0 /\\ f = a ]", 0-1) = a
	S("lbl52(a, b, c, d, e, f) -> lbl72(a, f, c, d - 1, e, f) [ d >= 1 /\\ a >= d /\\ b = 0 /\\ f = a ]", 0-2) = c
	S("lbl52(a, b, c, d, e, f) -> lbl72(a, f, c, d - 1, e, f) [ d >= 1 /\\ a >= d /\\ b = 0 /\\ f = a ]", 0-3) = a
	S("lbl52(a, b, c, d, e, f) -> lbl72(a, f, c, d - 1, e, f) [ d >= 1 /\\ a >= d /\\ b = 0 /\\ f = a ]", 0-4) = e
	S("lbl52(a, b, c, d, e, f) -> lbl72(a, f, c, d - 1, e, f) [ d >= 1 /\\ a >= d /\\ b = 0 /\\ f = a ]", 0-5) = a
	S("lbl52(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\\ b >= 1 /\\ b >= 0 /\\ a >= d /\\ f = a ]", 0-0) = a
	S("lbl52(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\\ b >= 1 /\\ b >= 0 /\\ a >= d /\\ f = a ]", 0-1) = a + c
	S("lbl52(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\\ b >= 1 /\\ b >= 0 /\\ a >= d /\\ f = a ]", 0-2) = c
	S("lbl52(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\\ b >= 1 /\\ b >= 0 /\\ a >= d /\\ f = a ]", 0-3) = a
	S("lbl52(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\\ b >= 1 /\\ b >= 0 /\\ a >= d /\\ f = a ]", 0-4) = e
	S("lbl52(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\\ b >= 1 /\\ b >= 0 /\\ a >= d /\\ f = a ]", 0-5) = a
	S("start(a, b, c, d, e, f) -> lbl72(a, f, c, f - 1, e, f) [ a >= 1 /\\ 0 >= c /\\ b = c /\\ d = e /\\ f = a ]", 0-0) = a
	S("start(a, b, c, d, e, f) -> lbl72(a, f, c, f - 1, e, f) [ a >= 1 /\\ 0 >= c /\\ b = c /\\ d = e /\\ f = a ]", 0-1) = a
	S("start(a, b, c, d, e, f) -> lbl72(a, f, c, f - 1, e, f) [ a >= 1 /\\ 0 >= c /\\ b = c /\\ d = e /\\ f = a ]", 0-2) = c
	S("start(a, b, c, d, e, f) -> lbl72(a, f, c, f - 1, e, f) [ a >= 1 /\\ 0 >= c /\\ b = c /\\ d = e /\\ f = a ]", 0-3) = a
	S("start(a, b, c, d, e, f) -> lbl72(a, f, c, f - 1, e, f) [ a >= 1 /\\ 0 >= c /\\ b = c /\\ d = e /\\ f = a ]", 0-4) = e
	S("start(a, b, c, d, e, f) -> lbl72(a, f, c, f - 1, e, f) [ a >= 1 /\\ 0 >= c /\\ b = c /\\ d = e /\\ f = a ]", 0-5) = a
	S("start(a, b, c, d, e, f) -> lbl52(a, b - 1, c, f, e, f) [ a >= 1 /\\ c >= 1 /\\ b = c /\\ d = e /\\ f = a ]", 0-0) = a
	S("start(a, b, c, d, e, f) -> lbl52(a, b - 1, c, f, e, f) [ a >= 1 /\\ c >= 1 /\\ b = c /\\ d = e /\\ f = a ]", 0-1) = c
	S("start(a, b, c, d, e, f) -> lbl52(a, b - 1, c, f, e, f) [ a >= 1 /\\ c >= 1 /\\ b = c /\\ d = e /\\ f = a ]", 0-2) = c
	S("start(a, b, c, d, e, f) -> lbl52(a, b - 1, c, f, e, f) [ a >= 1 /\\ c >= 1 /\\ b = c /\\ d = e /\\ f = a ]", 0-3) = a
	S("start(a, b, c, d, e, f) -> lbl52(a, b - 1, c, f, e, f) [ a >= 1 /\\ c >= 1 /\\ b = c /\\ d = e /\\ f = a ]", 0-4) = e
	S("start(a, b, c, d, e, f) -> lbl52(a, b - 1, c, f, e, f) [ a >= 1 /\\ c >= 1 /\\ b = c /\\ d = e /\\ f = a ]", 0-5) = a
orients the transition
	lbl52(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\ b >= 1 /\ b >= 0 /\ a >= d /\ f = a ]
weakly and the transition
	lbl52(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\ b >= 1 /\ b >= 0 /\ a >= d /\ f = a ]
strictly and produces the following problem:
6:	T:
		(1, 1)                      start(a, b, c, d, e, f) -> lbl52(a, b - 1, c, f, e, f) [ a >= 1 /\ c >= 1 /\ b = c /\ d = e /\ f = a ]
		(1, 1)                      start(a, b, c, d, e, f) -> lbl72(a, f, c, f - 1, e, f) [ a >= 1 /\ 0 >= c /\ b = c /\ d = e /\ f = a ]
		(2*a^2 + 4*a + c + 3, 1)    lbl52(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\ b >= 1 /\ b >= 0 /\ a >= d /\ f = a ]
		(2*a + 2, 1)                lbl52(a, b, c, d, e, f) -> lbl72(a, f, c, d - 1, e, f) [ d >= 1 /\ a >= d /\ b = 0 /\ f = a ]
		(2*a + 2, 1)                lbl72(a, b, c, d, e, f) -> lbl52(a, b - 1, c, d, e, f) [ d >= 1 /\ a >= 1 /\ d >= 0 /\ a >= d + 1 /\ f = a /\ b = a ]
		(1, 1)                      start0(a, b, c, d, e, f) -> start(a, c, c, e, e, a)
	start location:	start0
	leaf cost:	2

Complexity upper bound 2*a^2 + 8*a + c + 12

Time: 0.406 sec (SMT: 0.383 sec)