YES(?, 13*a + 2*a^2 + 17)

Initial complexity problem:
1:	T:
		(?, 1)    start(a, b, c, d, e, f) -> stop(a, b, c, f, e, f) [ 0 >= a + 1 /\ b = c /\ d = e /\ f = a ]
		(?, 1)    start(a, b, c, d, e, f) -> lbl121(a, 1, c, f - 1, e, f) [ a >= 0 /\ 1 >= a /\ b = c /\ d = e /\ f = a ]
		(?, 1)    start(a, b, c, d, e, f) -> lbl101(a, 2, c, f, e, f) [ a >= 2 /\ b = c /\ d = e /\ f = a ]
		(?, 1)    lbl121(a, b, c, d, e, f) -> stop(a, b, c, d, e, f) [ a >= 0 /\ b >= 0 /\ b >= 1 /\ d + 1 = 0 /\ f = a ]
		(?, 1)    lbl121(a, b, c, d, e, f) -> lbl121(a, 1, c, d - 1, e, f) [ d >= 0 /\ 1 >= d /\ a >= d + 1 /\ b >= d + 1 /\ b >= 1 /\ d + 1 >= 0 /\ f = a ]
		(?, 1)    lbl121(a, b, c, d, e, f) -> lbl101(a, 2, c, d, e, f) [ d >= 2 /\ a >= d + 1 /\ b >= d + 1 /\ b >= 1 /\ d + 1 >= 0 /\ f = a ]
		(?, 1)    lbl101(a, b, c, d, e, f) -> lbl101(a, 2*b, c, d, e, f) [ d >= b + 1 /\ b >= 2 /\ 2*d >= b + 2 /\ a >= d /\ f = a ]
		(?, 1)    lbl101(a, b, c, d, e, f) -> lbl121(a, b, c, d - 1, e, f) [ b >= d /\ b >= 2 /\ 2*d >= b + 2 /\ a >= d /\ f = 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 1 produces the following problem:
2:	T:
		(?, 1)    start(a, b, c, d, e, f) -> lbl121(a, 1, c, f - 1, e, f) [ a >= 0 /\ 1 >= a /\ b = c /\ d = e /\ f = a ]
		(?, 1)    start(a, b, c, d, e, f) -> lbl101(a, 2, c, f, e, f) [ a >= 2 /\ b = c /\ d = e /\ f = a ]
		(?, 1)    lbl121(a, b, c, d, e, f) -> lbl121(a, 1, c, d - 1, e, f) [ d >= 0 /\ 1 >= d /\ a >= d + 1 /\ b >= d + 1 /\ b >= 1 /\ d + 1 >= 0 /\ f = a ]
		(?, 1)    lbl121(a, b, c, d, e, f) -> lbl101(a, 2, c, d, e, f) [ d >= 2 /\ a >= d + 1 /\ b >= d + 1 /\ b >= 1 /\ d + 1 >= 0 /\ f = a ]
		(?, 1)    lbl101(a, b, c, d, e, f) -> lbl101(a, 2*b, c, d, e, f) [ d >= b + 1 /\ b >= 2 /\ 2*d >= b + 2 /\ a >= d /\ f = a ]
		(?, 1)    lbl101(a, b, c, d, e, f) -> lbl121(a, b, c, d - 1, e, f) [ b >= d /\ b >= 2 /\ 2*d >= b + 2 /\ a >= d /\ f = 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 2 produces the following problem:
3:	T:
		(1, 1)    start(a, b, c, d, e, f) -> lbl121(a, 1, c, f - 1, e, f) [ a >= 0 /\ 1 >= a /\ b = c /\ d = e /\ f = a ]
		(1, 1)    start(a, b, c, d, e, f) -> lbl101(a, 2, c, f, e, f) [ a >= 2 /\ b = c /\ d = e /\ f = a ]
		(?, 1)    lbl121(a, b, c, d, e, f) -> lbl121(a, 1, c, d - 1, e, f) [ d >= 0 /\ 1 >= d /\ a >= d + 1 /\ b >= d + 1 /\ b >= 1 /\ d + 1 >= 0 /\ f = a ]
		(?, 1)    lbl121(a, b, c, d, e, f) -> lbl101(a, 2, c, d, e, f) [ d >= 2 /\ a >= d + 1 /\ b >= d + 1 /\ b >= 1 /\ d + 1 >= 0 /\ f = a ]
		(?, 1)    lbl101(a, b, c, d, e, f) -> lbl101(a, 2*b, c, d, e, f) [ d >= b + 1 /\ b >= 2 /\ 2*d >= b + 2 /\ a >= d /\ f = a ]
		(?, 1)    lbl101(a, b, c, d, e, f) -> lbl121(a, b, c, d - 1, e, f) [ b >= d /\ b >= 2 /\ 2*d >= b + 2 /\ a >= d /\ f = 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(lbl121) = 2*V_4 + 3
	Pol(lbl101) = 2*V_4 + 2
	Pol(start0) = 2*V_1 + 2
orients all transitions weakly and the transitions
	lbl121(a, b, c, d, e, f) -> lbl121(a, 1, c, d - 1, e, f) [ d >= 0 /\ 1 >= d /\ a >= d + 1 /\ b >= d + 1 /\ b >= 1 /\ d + 1 >= 0 /\ f = a ]
	lbl121(a, b, c, d, e, f) -> lbl101(a, 2, c, d, e, f) [ d >= 2 /\ a >= d + 1 /\ b >= d + 1 /\ b >= 1 /\ d + 1 >= 0 /\ f = a ]
	lbl101(a, b, c, d, e, f) -> lbl121(a, b, c, d - 1, e, f) [ b >= d /\ b >= 2 /\ 2*d >= b + 2 /\ a >= d /\ f = a ]
strictly and produces the following problem:
4:	T:
		(1, 1)          start(a, b, c, d, e, f) -> lbl121(a, 1, c, f - 1, e, f) [ a >= 0 /\ 1 >= a /\ b = c /\ d = e /\ f = a ]
		(1, 1)          start(a, b, c, d, e, f) -> lbl101(a, 2, c, f, e, f) [ a >= 2 /\ b = c /\ d = e /\ f = a ]
		(2*a + 2, 1)    lbl121(a, b, c, d, e, f) -> lbl121(a, 1, c, d - 1, e, f) [ d >= 0 /\ 1 >= d /\ a >= d + 1 /\ b >= d + 1 /\ b >= 1 /\ d + 1 >= 0 /\ f = a ]
		(2*a + 2, 1)    lbl121(a, b, c, d, e, f) -> lbl101(a, 2, c, d, e, f) [ d >= 2 /\ a >= d + 1 /\ b >= d + 1 /\ b >= 1 /\ d + 1 >= 0 /\ f = a ]
		(?, 1)          lbl101(a, b, c, d, e, f) -> lbl101(a, 2*b, c, d, e, f) [ d >= b + 1 /\ b >= 2 /\ 2*d >= b + 2 /\ a >= d /\ f = a ]
		(2*a + 2, 1)    lbl101(a, b, c, d, e, f) -> lbl121(a, b, c, d - 1, e, f) [ b >= d /\ b >= 2 /\ 2*d >= b + 2 /\ a >= d /\ f = 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(lbl101) = -V_2 + V_4
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("lbl101(a, b, c, d, e, f) -> lbl121(a, b, c, d - 1, e, f) [ b >= d /\\ b >= 2 /\\ 2*d >= b + 2 /\\ a >= d /\\ f = a ]", 0-0) = a
	S("lbl101(a, b, c, d, e, f) -> lbl121(a, b, c, d - 1, e, f) [ b >= d /\\ b >= 2 /\\ 2*d >= b + 2 /\\ a >= d /\\ f = a ]", 0-1) = 2*a + 8
	S("lbl101(a, b, c, d, e, f) -> lbl121(a, b, c, d - 1, e, f) [ b >= d /\\ b >= 2 /\\ 2*d >= b + 2 /\\ a >= d /\\ f = a ]", 0-2) = c
	S("lbl101(a, b, c, d, e, f) -> lbl121(a, b, c, d - 1, e, f) [ b >= d /\\ b >= 2 /\\ 2*d >= b + 2 /\\ a >= d /\\ f = a ]", 0-3) = a
	S("lbl101(a, b, c, d, e, f) -> lbl121(a, b, c, d - 1, e, f) [ b >= d /\\ b >= 2 /\\ 2*d >= b + 2 /\\ a >= d /\\ f = a ]", 0-4) = e
	S("lbl101(a, b, c, d, e, f) -> lbl121(a, b, c, d - 1, e, f) [ b >= d /\\ b >= 2 /\\ 2*d >= b + 2 /\\ a >= d /\\ f = a ]", 0-5) = a
	S("lbl101(a, b, c, d, e, f) -> lbl101(a, 2*b, c, d, e, f) [ d >= b + 1 /\\ b >= 2 /\\ 2*d >= b + 2 /\\ a >= d /\\ f = a ]", 0-0) = a
	S("lbl101(a, b, c, d, e, f) -> lbl101(a, 2*b, c, d, e, f) [ d >= b + 1 /\\ b >= 2 /\\ 2*d >= b + 2 /\\ a >= d /\\ f = a ]", 0-1) = 2*a
	S("lbl101(a, b, c, d, e, f) -> lbl101(a, 2*b, c, d, e, f) [ d >= b + 1 /\\ b >= 2 /\\ 2*d >= b + 2 /\\ a >= d /\\ f = a ]", 0-2) = c
	S("lbl101(a, b, c, d, e, f) -> lbl101(a, 2*b, c, d, e, f) [ d >= b + 1 /\\ b >= 2 /\\ 2*d >= b + 2 /\\ a >= d /\\ f = a ]", 0-3) = a
	S("lbl101(a, b, c, d, e, f) -> lbl101(a, 2*b, c, d, e, f) [ d >= b + 1 /\\ b >= 2 /\\ 2*d >= b + 2 /\\ a >= d /\\ f = a ]", 0-4) = e
	S("lbl101(a, b, c, d, e, f) -> lbl101(a, 2*b, c, d, e, f) [ d >= b + 1 /\\ b >= 2 /\\ 2*d >= b + 2 /\\ a >= d /\\ f = a ]", 0-5) = a
	S("lbl121(a, b, c, d, e, f) -> lbl101(a, 2, c, d, e, f) [ d >= 2 /\\ a >= d + 1 /\\ b >= d + 1 /\\ b >= 1 /\\ d + 1 >= 0 /\\ f = a ]", 0-0) = a
	S("lbl121(a, b, c, d, e, f) -> lbl101(a, 2, c, d, e, f) [ d >= 2 /\\ a >= d + 1 /\\ b >= d + 1 /\\ b >= 1 /\\ d + 1 >= 0 /\\ f = a ]", 0-1) = 2
	S("lbl121(a, b, c, d, e, f) -> lbl101(a, 2, c, d, e, f) [ d >= 2 /\\ a >= d + 1 /\\ b >= d + 1 /\\ b >= 1 /\\ d + 1 >= 0 /\\ f = a ]", 0-2) = c
	S("lbl121(a, b, c, d, e, f) -> lbl101(a, 2, c, d, e, f) [ d >= 2 /\\ a >= d + 1 /\\ b >= d + 1 /\\ b >= 1 /\\ d + 1 >= 0 /\\ f = a ]", 0-3) = a
	S("lbl121(a, b, c, d, e, f) -> lbl101(a, 2, c, d, e, f) [ d >= 2 /\\ a >= d + 1 /\\ b >= d + 1 /\\ b >= 1 /\\ d + 1 >= 0 /\\ f = a ]", 0-4) = e
	S("lbl121(a, b, c, d, e, f) -> lbl101(a, 2, c, d, e, f) [ d >= 2 /\\ a >= d + 1 /\\ b >= d + 1 /\\ b >= 1 /\\ d + 1 >= 0 /\\ f = a ]", 0-5) = a
	S("lbl121(a, b, c, d, e, f) -> lbl121(a, 1, c, d - 1, e, f) [ d >= 0 /\\ 1 >= d /\\ a >= d + 1 /\\ b >= d + 1 /\\ b >= 1 /\\ d + 1 >= 0 /\\ f = a ]", 0-0) = a + 1
	S("lbl121(a, b, c, d, e, f) -> lbl121(a, 1, c, d - 1, e, f) [ d >= 0 /\\ 1 >= d /\\ a >= d + 1 /\\ b >= d + 1 /\\ b >= 1 /\\ d + 1 >= 0 /\\ f = a ]", 0-1) = 1
	S("lbl121(a, b, c, d, e, f) -> lbl121(a, 1, c, d - 1, e, f) [ d >= 0 /\\ 1 >= d /\\ a >= d + 1 /\\ b >= d + 1 /\\ b >= 1 /\\ d + 1 >= 0 /\\ f = a ]", 0-2) = c
	S("lbl121(a, b, c, d, e, f) -> lbl121(a, 1, c, d - 1, e, f) [ d >= 0 /\\ 1 >= d /\\ a >= d + 1 /\\ b >= d + 1 /\\ b >= 1 /\\ d + 1 >= 0 /\\ f = a ]", 0-3) = 1
	S("lbl121(a, b, c, d, e, f) -> lbl121(a, 1, c, d - 1, e, f) [ d >= 0 /\\ 1 >= d /\\ a >= d + 1 /\\ b >= d + 1 /\\ b >= 1 /\\ d + 1 >= 0 /\\ f = a ]", 0-4) = e
	S("lbl121(a, b, c, d, e, f) -> lbl121(a, 1, c, d - 1, e, f) [ d >= 0 /\\ 1 >= d /\\ a >= d + 1 /\\ b >= d + 1 /\\ b >= 1 /\\ d + 1 >= 0 /\\ f = a ]", 0-5) = a + 1
	S("start(a, b, c, d, e, f) -> lbl101(a, 2, c, f, e, f) [ a >= 2 /\\ b = c /\\ d = e /\\ f = a ]", 0-0) = a
	S("start(a, b, c, d, e, f) -> lbl101(a, 2, c, f, e, f) [ a >= 2 /\\ b = c /\\ d = e /\\ f = a ]", 0-1) = 2
	S("start(a, b, c, d, e, f) -> lbl101(a, 2, c, f, e, f) [ a >= 2 /\\ b = c /\\ d = e /\\ f = a ]", 0-2) = c
	S("start(a, b, c, d, e, f) -> lbl101(a, 2, c, f, e, f) [ a >= 2 /\\ b = c /\\ d = e /\\ f = a ]", 0-3) = a
	S("start(a, b, c, d, e, f) -> lbl101(a, 2, c, f, e, f) [ a >= 2 /\\ b = c /\\ d = e /\\ f = a ]", 0-4) = e
	S("start(a, b, c, d, e, f) -> lbl101(a, 2, c, f, e, f) [ a >= 2 /\\ b = c /\\ d = e /\\ f = a ]", 0-5) = a
	S("start(a, b, c, d, e, f) -> lbl121(a, 1, c, f - 1, e, f) [ a >= 0 /\\ 1 >= a /\\ b = c /\\ d = e /\\ f = a ]", 0-0) = 1
	S("start(a, b, c, d, e, f) -> lbl121(a, 1, c, f - 1, e, f) [ a >= 0 /\\ 1 >= a /\\ b = c /\\ d = e /\\ f = a ]", 0-1) = 1
	S("start(a, b, c, d, e, f) -> lbl121(a, 1, c, f - 1, e, f) [ a >= 0 /\\ 1 >= a /\\ b = c /\\ d = e /\\ f = a ]", 0-2) = c
	S("start(a, b, c, d, e, f) -> lbl121(a, 1, c, f - 1, e, f) [ a >= 0 /\\ 1 >= a /\\ b = c /\\ d = e /\\ f = a ]", 0-3) = 1
	S("start(a, b, c, d, e, f) -> lbl121(a, 1, c, f - 1, e, f) [ a >= 0 /\\ 1 >= a /\\ b = c /\\ d = e /\\ f = a ]", 0-4) = e
	S("start(a, b, c, d, e, f) -> lbl121(a, 1, c, f - 1, e, f) [ a >= 0 /\\ 1 >= a /\\ b = c /\\ d = e /\\ f = a ]", 0-5) = 1
orients the transition
	lbl101(a, b, c, d, e, f) -> lbl101(a, 2*b, c, d, e, f) [ d >= b + 1 /\ b >= 2 /\ 2*d >= b + 2 /\ a >= d /\ f = a ]
weakly and the transition
	lbl101(a, b, c, d, e, f) -> lbl101(a, 2*b, c, d, e, f) [ d >= b + 1 /\ b >= 2 /\ 2*d >= b + 2 /\ a >= d /\ f = a ]
strictly and produces the following problem:
5:	T:
		(1, 1)                  start(a, b, c, d, e, f) -> lbl121(a, 1, c, f - 1, e, f) [ a >= 0 /\ 1 >= a /\ b = c /\ d = e /\ f = a ]
		(1, 1)                  start(a, b, c, d, e, f) -> lbl101(a, 2, c, f, e, f) [ a >= 2 /\ b = c /\ d = e /\ f = a ]
		(2*a + 2, 1)            lbl121(a, b, c, d, e, f) -> lbl121(a, 1, c, d - 1, e, f) [ d >= 0 /\ 1 >= d /\ a >= d + 1 /\ b >= d + 1 /\ b >= 1 /\ d + 1 >= 0 /\ f = a ]
		(2*a + 2, 1)            lbl121(a, b, c, d, e, f) -> lbl101(a, 2, c, d, e, f) [ d >= 2 /\ a >= d + 1 /\ b >= d + 1 /\ b >= 1 /\ d + 1 >= 0 /\ f = a ]
		(2*a^2 + 7*a + 6, 1)    lbl101(a, b, c, d, e, f) -> lbl101(a, 2*b, c, d, e, f) [ d >= b + 1 /\ b >= 2 /\ 2*d >= b + 2 /\ a >= d /\ f = a ]
		(2*a + 2, 1)            lbl101(a, b, c, d, e, f) -> lbl121(a, b, c, d - 1, e, f) [ b >= d /\ b >= 2 /\ 2*d >= b + 2 /\ a >= d /\ f = 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 13*a + 2*a^2 + 17

Time: 0.501 sec (SMT: 0.474 sec)