YES(?, 4*a + 4*c + 4*e + 7)

Initial complexity problem:
1:	T:
		(?, 1)    start(a, b, c, d, e, f) -> stop(a, b, c, d, e, f) [ 0 >= a + 1 /\ b = c /\ d = e /\ f = a ]
		(?, 1)    start(a, b, c, d, e, f) -> stop(a, b, c, d, e, f) [ a >= 0 /\ c >= e + 1 /\ b = c /\ d = e /\ f = a ]
		(?, 1)    start(a, b, c, d, e, f) -> lbl91(a, b, c, d - f - 1, e, f) [ a >= 0 /\ e >= c /\ b = c /\ d = e /\ f = a ]
		(?, 1)    start(a, b, c, d, e, f) -> lbl101(a, f + b + 1, c, d, e, f) [ a >= 0 /\ e >= c /\ b = c /\ d = e /\ f = a ]
		(?, 1)    lbl91(a, b, c, d, e, f) -> stop(a, b, c, d, e, f) [ b >= d + 1 /\ b >= c /\ a >= 0 /\ a + d + 1 >= b /\ e >= a + d + 1 /\ f = a ]
		(?, 1)    lbl91(a, b, c, d, e, f) -> stop(a, b, c, d, e, f) [ d >= b /\ 0 >= a + 1 /\ b >= c /\ a >= 0 /\ a + d + 1 >= b /\ e >= a + d + 1 /\ f = a ]
		(?, 1)    lbl91(a, b, c, d, e, f) -> lbl91(a, b, c, d - f - 1, e, f) [ a >= 0 /\ d >= b /\ b >= c /\ a + d + 1 >= b /\ e >= a + d + 1 /\ f = a ]
		(?, 1)    lbl91(a, b, c, d, e, f) -> lbl101(a, f + b + 1, c, d, e, f) [ a >= 0 /\ d >= b /\ b >= c /\ a + d + 1 >= b /\ e >= a + d + 1 /\ f = a ]
		(?, 1)    lbl101(a, b, c, d, e, f) -> stop(a, b, c, d, e, f) [ b >= d + 1 /\ e >= d /\ a >= 0 /\ b >= a + c + 1 /\ a + d + 1 >= b /\ f = a ]
		(?, 1)    lbl101(a, b, c, d, e, f) -> stop(a, b, c, d, e, f) [ d >= b /\ 0 >= a + 1 /\ e >= d /\ a >= 0 /\ b >= a + c + 1 /\ a + d + 1 >= b /\ f = a ]
		(?, 1)    lbl101(a, b, c, d, e, f) -> lbl91(a, b, c, d - f - 1, e, f) [ a >= 0 /\ d >= b /\ e >= d /\ b >= a + c + 1 /\ a + d + 1 >= b /\ f = a ]
		(?, 1)    lbl101(a, b, c, d, e, f) -> lbl101(a, f + b + 1, c, d, e, f) [ a >= 0 /\ d >= b /\ e >= d /\ b >= a + c + 1 /\ a + d + 1 >= b /\ f = 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:
	lbl91(a, b, c, d, e, f) -> stop(a, b, c, d, e, f) [ d >= b /\ 0 >= a + 1 /\ b >= c /\ a >= 0 /\ a + d + 1 >= b /\ e >= a + d + 1 /\ f = a ]
	lbl101(a, b, c, d, e, f) -> stop(a, b, c, d, e, f) [ d >= b /\ 0 >= a + 1 /\ e >= d /\ a >= 0 /\ b >= a + c + 1 /\ a + d + 1 >= b /\ f = a ]
We thus obtain the following problem:
2:	T:
		(?, 1)    start(a, b, c, d, e, f) -> stop(a, b, c, d, e, f) [ 0 >= a + 1 /\ b = c /\ d = e /\ f = a ]
		(?, 1)    start(a, b, c, d, e, f) -> stop(a, b, c, d, e, f) [ a >= 0 /\ c >= e + 1 /\ b = c /\ d = e /\ f = a ]
		(?, 1)    start(a, b, c, d, e, f) -> lbl91(a, b, c, d - f - 1, e, f) [ a >= 0 /\ e >= c /\ b = c /\ d = e /\ f = a ]
		(?, 1)    start(a, b, c, d, e, f) -> lbl101(a, f + b + 1, c, d, e, f) [ a >= 0 /\ e >= c /\ b = c /\ d = e /\ f = a ]
		(?, 1)    lbl91(a, b, c, d, e, f) -> stop(a, b, c, d, e, f) [ b >= d + 1 /\ b >= c /\ a >= 0 /\ a + d + 1 >= b /\ e >= a + d + 1 /\ f = a ]
		(?, 1)    lbl91(a, b, c, d, e, f) -> lbl91(a, b, c, d - f - 1, e, f) [ a >= 0 /\ d >= b /\ b >= c /\ a + d + 1 >= b /\ e >= a + d + 1 /\ f = a ]
		(?, 1)    lbl91(a, b, c, d, e, f) -> lbl101(a, f + b + 1, c, d, e, f) [ a >= 0 /\ d >= b /\ b >= c /\ a + d + 1 >= b /\ e >= a + d + 1 /\ f = a ]
		(?, 1)    lbl101(a, b, c, d, e, f) -> stop(a, b, c, d, e, f) [ b >= d + 1 /\ e >= d /\ a >= 0 /\ b >= a + c + 1 /\ a + d + 1 >= b /\ f = a ]
		(?, 1)    lbl101(a, b, c, d, e, f) -> lbl91(a, b, c, d - f - 1, e, f) [ a >= 0 /\ d >= b /\ e >= d /\ b >= a + c + 1 /\ a + d + 1 >= b /\ f = a ]
		(?, 1)    lbl101(a, b, c, d, e, f) -> lbl101(a, f + b + 1, c, d, e, f) [ a >= 0 /\ d >= b /\ e >= d /\ b >= a + c + 1 /\ a + d + 1 >= b /\ 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 2 produces the following problem:
3:	T:
		(?, 1)    start(a, b, c, d, e, f) -> lbl91(a, b, c, d - f - 1, e, f) [ a >= 0 /\ e >= c /\ b = c /\ d = e /\ f = a ]
		(?, 1)    start(a, b, c, d, e, f) -> lbl101(a, f + b + 1, c, d, e, f) [ a >= 0 /\ e >= c /\ b = c /\ d = e /\ f = a ]
		(?, 1)    lbl91(a, b, c, d, e, f) -> lbl91(a, b, c, d - f - 1, e, f) [ a >= 0 /\ d >= b /\ b >= c /\ a + d + 1 >= b /\ e >= a + d + 1 /\ f = a ]
		(?, 1)    lbl91(a, b, c, d, e, f) -> lbl101(a, f + b + 1, c, d, e, f) [ a >= 0 /\ d >= b /\ b >= c /\ a + d + 1 >= b /\ e >= a + d + 1 /\ f = a ]
		(?, 1)    lbl101(a, b, c, d, e, f) -> lbl91(a, b, c, d - f - 1, e, f) [ a >= 0 /\ d >= b /\ e >= d /\ b >= a + c + 1 /\ a + d + 1 >= b /\ f = a ]
		(?, 1)    lbl101(a, b, c, d, e, f) -> lbl101(a, f + b + 1, c, d, e, f) [ a >= 0 /\ d >= b /\ e >= d /\ b >= a + c + 1 /\ a + d + 1 >= b /\ f = a ]
		(1, 1)    start0(a, b, c, d, e, f) -> start(a, c, c, e, e, a)
	start location:	start0
	leaf cost:	4

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

A polynomial rank function with
	Pol(start) = -V_2 + V_4 - V_6
	Pol(lbl91) = -V_2 + V_4 + 1
	Pol(lbl101) = -V_2 + V_4 + 1
	Pol(start0) = -V_1 - V_3 + V_5
orients all transitions weakly and the transitions
	lbl91(a, b, c, d, e, f) -> lbl91(a, b, c, d - f - 1, e, f) [ a >= 0 /\ d >= b /\ b >= c /\ a + d + 1 >= b /\ e >= a + d + 1 /\ f = a ]
	lbl91(a, b, c, d, e, f) -> lbl101(a, f + b + 1, c, d, e, f) [ a >= 0 /\ d >= b /\ b >= c /\ a + d + 1 >= b /\ e >= a + d + 1 /\ f = a ]
	lbl101(a, b, c, d, e, f) -> lbl91(a, b, c, d - f - 1, e, f) [ a >= 0 /\ d >= b /\ e >= d /\ b >= a + c + 1 /\ a + d + 1 >= b /\ f = a ]
	lbl101(a, b, c, d, e, f) -> lbl101(a, f + b + 1, c, d, e, f) [ a >= 0 /\ d >= b /\ e >= d /\ b >= a + c + 1 /\ a + d + 1 >= b /\ f = a ]
strictly and produces the following problem:
5:	T:
		(1, 1)            start(a, b, c, d, e, f) -> lbl91(a, b, c, d - f - 1, e, f) [ a >= 0 /\ e >= c /\ b = c /\ d = e /\ f = a ]
		(1, 1)            start(a, b, c, d, e, f) -> lbl101(a, f + b + 1, c, d, e, f) [ a >= 0 /\ e >= c /\ b = c /\ d = e /\ f = a ]
		(a + c + e, 1)    lbl91(a, b, c, d, e, f) -> lbl91(a, b, c, d - f - 1, e, f) [ a >= 0 /\ d >= b /\ b >= c /\ a + d + 1 >= b /\ e >= a + d + 1 /\ f = a ]
		(a + c + e, 1)    lbl91(a, b, c, d, e, f) -> lbl101(a, f + b + 1, c, d, e, f) [ a >= 0 /\ d >= b /\ b >= c /\ a + d + 1 >= b /\ e >= a + d + 1 /\ f = a ]
		(a + c + e, 1)    lbl101(a, b, c, d, e, f) -> lbl91(a, b, c, d - f - 1, e, f) [ a >= 0 /\ d >= b /\ e >= d /\ b >= a + c + 1 /\ a + d + 1 >= b /\ f = a ]
		(a + c + e, 1)    lbl101(a, b, c, d, e, f) -> lbl101(a, f + b + 1, c, d, e, f) [ a >= 0 /\ d >= b /\ e >= d /\ b >= a + c + 1 /\ a + d + 1 >= b /\ f = a ]
		(1, 1)            start0(a, b, c, d, e, f) -> start(a, c, c, e, e, a)
	start location:	start0
	leaf cost:	4

Complexity upper bound 4*a + 4*c + 4*e + 7

Time: 0.827 sec (SMT: 0.789 sec)