YES(?, 126)

Initial complexity problem:
1:	T:
		(?, 1)    start(a, b, c, d, e, f) -> lbl91(a, b, 100, d, 1, f) [ a = 0 /\ b = 0 /\ c = d /\ e = f ]
		(?, 1)    start(a, b, c, d, e, f) -> lbl111(a, b, 100, d, 2, f) [ 0 >= b + 1 /\ a = b /\ c = d /\ e = f ]
		(?, 1)    start(a, b, c, d, e, f) -> lbl111(a, b, 100, d, 2, f) [ b >= 1 /\ a = b /\ c = d /\ e = f ]
		(?, 1)    lbl91(a, b, c, d, e, f) -> stop(a, b, c, d, e, f) [ e = 40 /\ c = 100 /\ a = 0 /\ b = 0 ]
		(?, 1)    lbl91(a, b, c, d, e, f) -> lbl91(a, b, c, d, e + 1, f) [ 39 >= e /\ e >= 1 /\ 40 >= e /\ a = 0 /\ c = 100 /\ b = 0 ]
		(?, 1)    lbl91(a, b, c, d, e, f) -> lbl111(a, b, c, d, e + 2, f) [ 0 >= 1 /\ 39 >= e /\ e >= 1 /\ 40 >= e /\ c = 100 /\ a = 0 /\ b = 0 ]
		(?, 1)    lbl91(a, b, c, d, e, f) -> lbl111(a, b, c, d, e + 2, f) [ 0 >= 1 /\ 39 >= e /\ e >= 1 /\ 40 >= e /\ c = 100 /\ a = 0 /\ b = 0 ]
		(?, 1)    lbl111(a, b, c, d, e, f) -> stop(a, b, c, d, e, f) [ e >= 40 /\ e >= 2 /\ 41 >= e /\ c = 100 /\ a = b ]
		(?, 1)    lbl111(a, b, c, d, e, f) -> lbl91(a, b, c, d, e + 1, f) [ 39 >= e /\ e >= 2 /\ 41 >= e /\ a = 0 /\ c = 100 /\ b = 0 ]
		(?, 1)    lbl111(a, b, c, d, e, f) -> lbl111(a, b, c, d, e + 2, f) [ 0 >= b + 1 /\ 39 >= e /\ e >= 2 /\ 41 >= e /\ c = 100 /\ a = b ]
		(?, 1)    lbl111(a, b, c, d, e, f) -> lbl111(a, b, c, d, e + 2, f) [ b >= 1 /\ 39 >= e /\ e >= 2 /\ 41 >= e /\ c = 100 /\ a = b ]
		(1, 1)    start0(a, b, c, d, e, f) -> start(b, b, d, d, f, f)
	start location:	start0
	leaf cost:	0

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

Testing for reachability in the complexity graph removes the following transition from problem 3:
	lbl111(a, b, c, d, e, f) -> lbl91(a, b, c, d, e + 1, f) [ 39 >= e /\ e >= 2 /\ 41 >= e /\ a = 0 /\ c = 100 /\ b = 0 ]
We thus obtain the following problem:
4:	T:
		(?, 1)    lbl111(a, b, c, d, e, f) -> lbl111(a, b, c, d, e + 2, f) [ b >= 1 /\ 39 >= e /\ e >= 2 /\ 41 >= e /\ c = 100 /\ a = b ]
		(?, 1)    lbl111(a, b, c, d, e, f) -> lbl111(a, b, c, d, e + 2, f) [ 0 >= b + 1 /\ 39 >= e /\ e >= 2 /\ 41 >= e /\ c = 100 /\ a = b ]
		(?, 1)    lbl91(a, b, c, d, e, f) -> lbl91(a, b, c, d, e + 1, f) [ 39 >= e /\ e >= 1 /\ 40 >= e /\ a = 0 /\ c = 100 /\ b = 0 ]
		(?, 1)    start(a, b, c, d, e, f) -> lbl111(a, b, 100, d, 2, f) [ b >= 1 /\ a = b /\ c = d /\ e = f ]
		(?, 1)    start(a, b, c, d, e, f) -> lbl111(a, b, 100, d, 2, f) [ 0 >= b + 1 /\ a = b /\ c = d /\ e = f ]
		(?, 1)    start(a, b, c, d, e, f) -> lbl91(a, b, 100, d, 1, f) [ a = 0 /\ b = 0 /\ c = d /\ e = f ]
		(1, 1)    start0(a, b, c, d, e, f) -> start(b, b, d, d, f, f)
	start location:	start0
	leaf cost:	2

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

A polynomial rank function with
	Pol(lbl111) = -V_5 + 42
	Pol(lbl91) = -V_5 + 41
	Pol(start) = 40
	Pol(start0) = 40
orients all transitions weakly and the transitions
	lbl91(a, b, c, d, e, f) -> lbl91(a, b, c, d, e + 1, f) [ 39 >= e /\ e >= 1 /\ 40 >= e /\ a = 0 /\ c = 100 /\ b = 0 ]
	lbl111(a, b, c, d, e, f) -> lbl111(a, b, c, d, e + 2, f) [ b >= 1 /\ 39 >= e /\ e >= 2 /\ 41 >= e /\ c = 100 /\ a = b ]
	lbl111(a, b, c, d, e, f) -> lbl111(a, b, c, d, e + 2, f) [ 0 >= b + 1 /\ 39 >= e /\ e >= 2 /\ 41 >= e /\ c = 100 /\ a = b ]
strictly and produces the following problem:
6:	T:
		(40, 1)    lbl111(a, b, c, d, e, f) -> lbl111(a, b, c, d, e + 2, f) [ b >= 1 /\ 39 >= e /\ e >= 2 /\ 41 >= e /\ c = 100 /\ a = b ]
		(40, 1)    lbl111(a, b, c, d, e, f) -> lbl111(a, b, c, d, e + 2, f) [ 0 >= b + 1 /\ 39 >= e /\ e >= 2 /\ 41 >= e /\ c = 100 /\ a = b ]
		(40, 1)    lbl91(a, b, c, d, e, f) -> lbl91(a, b, c, d, e + 1, f) [ 39 >= e /\ e >= 1 /\ 40 >= e /\ a = 0 /\ c = 100 /\ b = 0 ]
		(1, 1)     start(a, b, c, d, e, f) -> lbl111(a, b, 100, d, 2, f) [ b >= 1 /\ a = b /\ c = d /\ e = f ]
		(1, 1)     start(a, b, c, d, e, f) -> lbl111(a, b, 100, d, 2, f) [ 0 >= b + 1 /\ a = b /\ c = d /\ e = f ]
		(1, 1)     start(a, b, c, d, e, f) -> lbl91(a, b, 100, d, 1, f) [ a = 0 /\ b = 0 /\ c = d /\ e = f ]
		(1, 1)     start0(a, b, c, d, e, f) -> start(b, b, d, d, f, f)
	start location:	start0
	leaf cost:	2

Complexity upper bound 126

Time: 0.619 sec (SMT: 0.589 sec)