YES(?, 2*a^2 + 10*a + 14)

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

Testing for unsatisfiable constraints removes the following transitions from problem 1:
	cut(a, b, c, d, e, f) -> cut(a, b, 0, d, e + 1, f) [ 1 >= a /\ a >= e + 3 /\ a >= e + 2 /\ e >= 1 /\ c + 1 = a /\ b = a ]
	cut(a, b, c, d, e, f) -> stop(a, b, 0, d, e + 1, f) [ 1 >= a /\ a >= 3 /\ c + 1 = a /\ e + 2 = a /\ b = a ]
We thus obtain the following problem:
2:	T:
		(?, 1)    start(a, b, c, d, e, f) -> lbl71(a, b, 1, d, 0, f) [ a >= 2 /\ b = a /\ c = d /\ e = f ]
		(?, 1)    start(a, b, c, d, e, f) -> stop(a, b, 0, d, 1, f) [ 1 >= a /\ b = a /\ c = d /\ e = f ]
		(?, 1)    lbl71(a, b, c, d, e, f) -> lbl71(a, b, c + 1, d, e, f) [ a >= c + 2 /\ a >= c + 1 /\ a >= e + 2 /\ c >= 1 /\ e >= 0 /\ b = a ]
		(?, 1)    lbl71(a, b, c, d, e, f) -> cut(a, b, c, d, e + 1, f) [ a >= e + 3 /\ a >= e + 2 /\ a >= 2 /\ e >= 0 /\ c + 1 = a /\ b = a ]
		(?, 1)    lbl71(a, b, c, d, e, f) -> stop(a, b, c, d, e + 1, f) [ a >= 2 /\ e + 2 = a /\ c + 1 = a /\ b = a ]
		(?, 1)    cut(a, b, c, d, e, f) -> lbl71(a, b, 1, d, e, f) [ a >= 2 /\ a >= e + 2 /\ e >= 1 /\ c + 1 = a /\ b = a ]
		(1, 1)    start0(a, b, c, d, e, f) -> start(a, a, d, d, f, f)
	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) -> lbl71(a, b, 1, d, 0, f) [ a >= 2 /\ b = a /\ c = d /\ e = f ]
		(?, 1)    lbl71(a, b, c, d, e, f) -> lbl71(a, b, c + 1, d, e, f) [ a >= c + 2 /\ a >= c + 1 /\ a >= e + 2 /\ c >= 1 /\ e >= 0 /\ b = a ]
		(?, 1)    lbl71(a, b, c, d, e, f) -> cut(a, b, c, d, e + 1, f) [ a >= e + 3 /\ a >= e + 2 /\ a >= 2 /\ e >= 0 /\ c + 1 = a /\ b = a ]
		(?, 1)    cut(a, b, c, d, e, f) -> lbl71(a, b, 1, d, e, f) [ a >= 2 /\ a >= e + 2 /\ e >= 1 /\ c + 1 = a /\ b = a ]
		(1, 1)    start0(a, b, c, d, e, f) -> start(a, a, d, d, f, f)
	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) -> lbl71(a, b, 1, d, 0, f) [ a >= 2 /\ b = a /\ c = d /\ e = f ]
		(?, 1)    lbl71(a, b, c, d, e, f) -> lbl71(a, b, c + 1, d, e, f) [ a >= c + 2 /\ a >= c + 1 /\ a >= e + 2 /\ c >= 1 /\ e >= 0 /\ b = a ]
		(?, 1)    lbl71(a, b, c, d, e, f) -> cut(a, b, c, d, e + 1, f) [ a >= e + 3 /\ a >= e + 2 /\ a >= 2 /\ e >= 0 /\ c + 1 = a /\ b = a ]
		(?, 1)    cut(a, b, c, d, e, f) -> lbl71(a, b, 1, d, e, f) [ a >= 2 /\ a >= e + 2 /\ e >= 1 /\ c + 1 = a /\ b = a ]
		(1, 1)    start0(a, b, c, d, e, f) -> start(a, a, d, d, f, f)
	start location:	start0
	leaf cost:	2

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

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

Complexity upper bound 2*a^2 + 10*a + 14

Time: 0.283 sec (SMT: 0.265 sec)