YES(?, 248*a + 45*c + 8960)

Initial complexity problem:
1:	T:
		(?, 1)    start(a, b, c, d) -> stop(a, b, c, d) [ a >= 30 /\ b = c /\ d = a ]
		(?, 1)    start(a, b, c, d) -> lbl171(a, b - 10, c, d + 2) [ c >= a /\ 29 >= a /\ b = c /\ d = a ]
		(?, 1)    start(a, b, c, d) -> lbl151(a, b + 7, c, d + 1) [ a >= c + 1 /\ c >= 6 /\ 29 >= a /\ b = c /\ d = a ]
		(?, 1)    start(a, b, c, d) -> lbl151(a, b + 2, c, d + 1) [ a >= c + 1 /\ 5 >= c /\ 29 >= a /\ b = c /\ d = a ]
		(?, 1)    lbl171(a, b, c, d) -> stop(a, b, c, d) [ d >= 30 /\ 29 >= a /\ 5*d + b >= 5*a + c /\ 7*d + c >= b + 7*a + 24 /\ 7*b + 1674 >= 19*d + 35*a + 7*c /\ b + 12 >= d ]
		(?, 1)    lbl171(a, b, c, d) -> lbl171(a, b - 10, c, d + 2) [ b >= d /\ 29 >= d /\ 29 >= a /\ 5*d + b >= 5*a + c /\ 7*d + c >= b + 7*a + 24 /\ 7*b + 1674 >= 19*d + 35*a + 7*c /\ b + 12 >= d ]
		(?, 1)    lbl171(a, b, c, d) -> lbl151(a, b + 7, c, d + 1) [ d >= b + 1 /\ b >= 6 /\ 29 >= d /\ 29 >= a /\ 5*d + b >= 5*a + c /\ 7*d + c >= b + 7*a + 24 /\ 7*b + 1674 >= 19*d + 35*a + 7*c /\ b + 12 >= d ]
		(?, 1)    lbl171(a, b, c, d) -> lbl151(a, b + 2, c, d + 1) [ d >= b + 1 /\ 5 >= b /\ 29 >= d /\ 29 >= a /\ 5*d + b >= 5*a + c /\ 7*d + c >= b + 7*a + 24 /\ 7*b + 1674 >= 19*d + 35*a + 7*c /\ b + 12 >= d ]
		(?, 1)    lbl151(a, b, c, d) -> lbl171(a, b - 10, c, d + 2) [ b >= d /\ 6*d >= 5*a + c + 7 /\ 5*d + b >= 5*a + c + 7 /\ d >= a + 1 /\ 29 >= a /\ b + 203 >= 2*d + 5*a + c /\ 2*b + 1561 >= 14*d + 35*a + 7*c /\ 140*d + 23*b >= 140*a + 28*c + 161 /\ 23*b + 5719 >= 56*d + 140*a + 28*c /\ d + 5 >= b /\ 7*d + c >= b + 7*a ]
		(?, 1)    lbl151(a, b, c, d) -> lbl151(a, b + 7, c, d + 1) [ d >= b + 1 /\ b >= 6 /\ 6*d >= 5*a + c + 7 /\ 5*d + b >= 5*a + c + 7 /\ d >= a + 1 /\ 29 >= a /\ b + 203 >= 2*d + 5*a + c /\ 2*b + 1561 >= 14*d + 35*a + 7*c /\ 140*d + 23*b >= 140*a + 28*c + 161 /\ 23*b + 5719 >= 56*d + 140*a + 28*c /\ d + 5 >= b /\ 7*d + c >= b + 7*a ]
		(?, 1)    lbl151(a, b, c, d) -> lbl151(a, b + 2, c, d + 1) [ d >= b + 1 /\ 5 >= b /\ 6*d >= 5*a + c + 7 /\ 5*d + b >= 5*a + c + 7 /\ d >= a + 1 /\ 29 >= a /\ b + 203 >= 2*d + 5*a + c /\ 2*b + 1561 >= 14*d + 35*a + 7*c /\ 140*d + 23*b >= 140*a + 28*c + 161 /\ 23*b + 5719 >= 56*d + 140*a + 28*c /\ d + 5 >= b /\ 7*d + c >= b + 7*a ]
		(1, 1)    start0(a, b, c, d) -> start(a, c, c, 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) -> lbl171(a, b - 10, c, d + 2) [ c >= a /\ 29 >= a /\ b = c /\ d = a ]
		(?, 1)    start(a, b, c, d) -> lbl151(a, b + 7, c, d + 1) [ a >= c + 1 /\ c >= 6 /\ 29 >= a /\ b = c /\ d = a ]
		(?, 1)    start(a, b, c, d) -> lbl151(a, b + 2, c, d + 1) [ a >= c + 1 /\ 5 >= c /\ 29 >= a /\ b = c /\ d = a ]
		(?, 1)    lbl171(a, b, c, d) -> lbl171(a, b - 10, c, d + 2) [ b >= d /\ 29 >= d /\ 29 >= a /\ 5*d + b >= 5*a + c /\ 7*d + c >= b + 7*a + 24 /\ 7*b + 1674 >= 19*d + 35*a + 7*c /\ b + 12 >= d ]
		(?, 1)    lbl171(a, b, c, d) -> lbl151(a, b + 7, c, d + 1) [ d >= b + 1 /\ b >= 6 /\ 29 >= d /\ 29 >= a /\ 5*d + b >= 5*a + c /\ 7*d + c >= b + 7*a + 24 /\ 7*b + 1674 >= 19*d + 35*a + 7*c /\ b + 12 >= d ]
		(?, 1)    lbl171(a, b, c, d) -> lbl151(a, b + 2, c, d + 1) [ d >= b + 1 /\ 5 >= b /\ 29 >= d /\ 29 >= a /\ 5*d + b >= 5*a + c /\ 7*d + c >= b + 7*a + 24 /\ 7*b + 1674 >= 19*d + 35*a + 7*c /\ b + 12 >= d ]
		(?, 1)    lbl151(a, b, c, d) -> lbl171(a, b - 10, c, d + 2) [ b >= d /\ 6*d >= 5*a + c + 7 /\ 5*d + b >= 5*a + c + 7 /\ d >= a + 1 /\ 29 >= a /\ b + 203 >= 2*d + 5*a + c /\ 2*b + 1561 >= 14*d + 35*a + 7*c /\ 140*d + 23*b >= 140*a + 28*c + 161 /\ 23*b + 5719 >= 56*d + 140*a + 28*c /\ d + 5 >= b /\ 7*d + c >= b + 7*a ]
		(?, 1)    lbl151(a, b, c, d) -> lbl151(a, b + 7, c, d + 1) [ d >= b + 1 /\ b >= 6 /\ 6*d >= 5*a + c + 7 /\ 5*d + b >= 5*a + c + 7 /\ d >= a + 1 /\ 29 >= a /\ b + 203 >= 2*d + 5*a + c /\ 2*b + 1561 >= 14*d + 35*a + 7*c /\ 140*d + 23*b >= 140*a + 28*c + 161 /\ 23*b + 5719 >= 56*d + 140*a + 28*c /\ d + 5 >= b /\ 7*d + c >= b + 7*a ]
		(?, 1)    lbl151(a, b, c, d) -> lbl151(a, b + 2, c, d + 1) [ d >= b + 1 /\ 5 >= b /\ 6*d >= 5*a + c + 7 /\ 5*d + b >= 5*a + c + 7 /\ d >= a + 1 /\ 29 >= a /\ b + 203 >= 2*d + 5*a + c /\ 2*b + 1561 >= 14*d + 35*a + 7*c /\ 140*d + 23*b >= 140*a + 28*c + 161 /\ 23*b + 5719 >= 56*d + 140*a + 28*c /\ d + 5 >= b /\ 7*d + c >= b + 7*a ]
		(1, 1)    start0(a, b, c, d) -> start(a, c, c, 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) -> lbl171(a, b - 10, c, d + 2) [ c >= a /\ 29 >= a /\ b = c /\ d = a ]
		(1, 1)    start(a, b, c, d) -> lbl151(a, b + 7, c, d + 1) [ a >= c + 1 /\ c >= 6 /\ 29 >= a /\ b = c /\ d = a ]
		(1, 1)    start(a, b, c, d) -> lbl151(a, b + 2, c, d + 1) [ a >= c + 1 /\ 5 >= c /\ 29 >= a /\ b = c /\ d = a ]
		(?, 1)    lbl171(a, b, c, d) -> lbl171(a, b - 10, c, d + 2) [ b >= d /\ 29 >= d /\ 29 >= a /\ 5*d + b >= 5*a + c /\ 7*d + c >= b + 7*a + 24 /\ 7*b + 1674 >= 19*d + 35*a + 7*c /\ b + 12 >= d ]
		(?, 1)    lbl171(a, b, c, d) -> lbl151(a, b + 7, c, d + 1) [ d >= b + 1 /\ b >= 6 /\ 29 >= d /\ 29 >= a /\ 5*d + b >= 5*a + c /\ 7*d + c >= b + 7*a + 24 /\ 7*b + 1674 >= 19*d + 35*a + 7*c /\ b + 12 >= d ]
		(?, 1)    lbl171(a, b, c, d) -> lbl151(a, b + 2, c, d + 1) [ d >= b + 1 /\ 5 >= b /\ 29 >= d /\ 29 >= a /\ 5*d + b >= 5*a + c /\ 7*d + c >= b + 7*a + 24 /\ 7*b + 1674 >= 19*d + 35*a + 7*c /\ b + 12 >= d ]
		(?, 1)    lbl151(a, b, c, d) -> lbl171(a, b - 10, c, d + 2) [ b >= d /\ 6*d >= 5*a + c + 7 /\ 5*d + b >= 5*a + c + 7 /\ d >= a + 1 /\ 29 >= a /\ b + 203 >= 2*d + 5*a + c /\ 2*b + 1561 >= 14*d + 35*a + 7*c /\ 140*d + 23*b >= 140*a + 28*c + 161 /\ 23*b + 5719 >= 56*d + 140*a + 28*c /\ d + 5 >= b /\ 7*d + c >= b + 7*a ]
		(?, 1)    lbl151(a, b, c, d) -> lbl151(a, b + 7, c, d + 1) [ d >= b + 1 /\ b >= 6 /\ 6*d >= 5*a + c + 7 /\ 5*d + b >= 5*a + c + 7 /\ d >= a + 1 /\ 29 >= a /\ b + 203 >= 2*d + 5*a + c /\ 2*b + 1561 >= 14*d + 35*a + 7*c /\ 140*d + 23*b >= 140*a + 28*c + 161 /\ 23*b + 5719 >= 56*d + 140*a + 28*c /\ d + 5 >= b /\ 7*d + c >= b + 7*a ]
		(?, 1)    lbl151(a, b, c, d) -> lbl151(a, b + 2, c, d + 1) [ d >= b + 1 /\ 5 >= b /\ 6*d >= 5*a + c + 7 /\ 5*d + b >= 5*a + c + 7 /\ d >= a + 1 /\ 29 >= a /\ b + 203 >= 2*d + 5*a + c /\ 2*b + 1561 >= 14*d + 35*a + 7*c /\ 140*d + 23*b >= 140*a + 28*c + 161 /\ 23*b + 5719 >= 56*d + 140*a + 28*c /\ d + 5 >= b /\ 7*d + c >= b + 7*a ]
		(1, 1)    start0(a, b, c, d) -> start(a, c, c, a)
	start location:	start0
	leaf cost:	2

A polynomial rank function with
	Pol(start) = -40*V_1 - V_2 - 8*V_3 - 7*V_4 + 1720
	Pol(lbl171) = -40*V_1 - V_2 - 8*V_3 - 7*V_4 + 1724
	Pol(lbl151) = -40*V_1 - V_2 - 8*V_3 - 7*V_4 + 1721
	Pol(start0) = -47*V_1 - 9*V_3 + 1720
orients all transitions weakly and the transitions
	lbl171(a, b, c, d) -> lbl151(a, b + 7, c, d + 1) [ d >= b + 1 /\ b >= 6 /\ 29 >= d /\ 29 >= a /\ 5*d + b >= 5*a + c /\ 7*d + c >= b + 7*a + 24 /\ 7*b + 1674 >= 19*d + 35*a + 7*c /\ b + 12 >= d ]
	lbl171(a, b, c, d) -> lbl151(a, b + 2, c, d + 1) [ d >= b + 1 /\ 5 >= b /\ 29 >= d /\ 29 >= a /\ 5*d + b >= 5*a + c /\ 7*d + c >= b + 7*a + 24 /\ 7*b + 1674 >= 19*d + 35*a + 7*c /\ b + 12 >= d ]
	lbl151(a, b, c, d) -> lbl171(a, b - 10, c, d + 2) [ b >= d /\ 6*d >= 5*a + c + 7 /\ 5*d + b >= 5*a + c + 7 /\ d >= a + 1 /\ 29 >= a /\ b + 203 >= 2*d + 5*a + c /\ 2*b + 1561 >= 14*d + 35*a + 7*c /\ 140*d + 23*b >= 140*a + 28*c + 161 /\ 23*b + 5719 >= 56*d + 140*a + 28*c /\ d + 5 >= b /\ 7*d + c >= b + 7*a ]
	lbl151(a, b, c, d) -> lbl151(a, b + 7, c, d + 1) [ d >= b + 1 /\ b >= 6 /\ 6*d >= 5*a + c + 7 /\ 5*d + b >= 5*a + c + 7 /\ d >= a + 1 /\ 29 >= a /\ b + 203 >= 2*d + 5*a + c /\ 2*b + 1561 >= 14*d + 35*a + 7*c /\ 140*d + 23*b >= 140*a + 28*c + 161 /\ 23*b + 5719 >= 56*d + 140*a + 28*c /\ d + 5 >= b /\ 7*d + c >= b + 7*a ]
	lbl151(a, b, c, d) -> lbl151(a, b + 2, c, d + 1) [ d >= b + 1 /\ 5 >= b /\ 6*d >= 5*a + c + 7 /\ 5*d + b >= 5*a + c + 7 /\ d >= a + 1 /\ 29 >= a /\ b + 203 >= 2*d + 5*a + c /\ 2*b + 1561 >= 14*d + 35*a + 7*c /\ 140*d + 23*b >= 140*a + 28*c + 161 /\ 23*b + 5719 >= 56*d + 140*a + 28*c /\ d + 5 >= b /\ 7*d + c >= b + 7*a ]
strictly and produces the following problem:
4:	T:
		(1, 1)                    start(a, b, c, d) -> lbl171(a, b - 10, c, d + 2) [ c >= a /\ 29 >= a /\ b = c /\ d = a ]
		(1, 1)                    start(a, b, c, d) -> lbl151(a, b + 7, c, d + 1) [ a >= c + 1 /\ c >= 6 /\ 29 >= a /\ b = c /\ d = a ]
		(1, 1)                    start(a, b, c, d) -> lbl151(a, b + 2, c, d + 1) [ a >= c + 1 /\ 5 >= c /\ 29 >= a /\ b = c /\ d = a ]
		(?, 1)                    lbl171(a, b, c, d) -> lbl171(a, b - 10, c, d + 2) [ b >= d /\ 29 >= d /\ 29 >= a /\ 5*d + b >= 5*a + c /\ 7*d + c >= b + 7*a + 24 /\ 7*b + 1674 >= 19*d + 35*a + 7*c /\ b + 12 >= d ]
		(47*a + 9*c + 1720, 1)    lbl171(a, b, c, d) -> lbl151(a, b + 7, c, d + 1) [ d >= b + 1 /\ b >= 6 /\ 29 >= d /\ 29 >= a /\ 5*d + b >= 5*a + c /\ 7*d + c >= b + 7*a + 24 /\ 7*b + 1674 >= 19*d + 35*a + 7*c /\ b + 12 >= d ]
		(47*a + 9*c + 1720, 1)    lbl171(a, b, c, d) -> lbl151(a, b + 2, c, d + 1) [ d >= b + 1 /\ 5 >= b /\ 29 >= d /\ 29 >= a /\ 5*d + b >= 5*a + c /\ 7*d + c >= b + 7*a + 24 /\ 7*b + 1674 >= 19*d + 35*a + 7*c /\ b + 12 >= d ]
		(47*a + 9*c + 1720, 1)    lbl151(a, b, c, d) -> lbl171(a, b - 10, c, d + 2) [ b >= d /\ 6*d >= 5*a + c + 7 /\ 5*d + b >= 5*a + c + 7 /\ d >= a + 1 /\ 29 >= a /\ b + 203 >= 2*d + 5*a + c /\ 2*b + 1561 >= 14*d + 35*a + 7*c /\ 140*d + 23*b >= 140*a + 28*c + 161 /\ 23*b + 5719 >= 56*d + 140*a + 28*c /\ d + 5 >= b /\ 7*d + c >= b + 7*a ]
		(47*a + 9*c + 1720, 1)    lbl151(a, b, c, d) -> lbl151(a, b + 7, c, d + 1) [ d >= b + 1 /\ b >= 6 /\ 6*d >= 5*a + c + 7 /\ 5*d + b >= 5*a + c + 7 /\ d >= a + 1 /\ 29 >= a /\ b + 203 >= 2*d + 5*a + c /\ 2*b + 1561 >= 14*d + 35*a + 7*c /\ 140*d + 23*b >= 140*a + 28*c + 161 /\ 23*b + 5719 >= 56*d + 140*a + 28*c /\ d + 5 >= b /\ 7*d + c >= b + 7*a ]
		(47*a + 9*c + 1720, 1)    lbl151(a, b, c, d) -> lbl151(a, b + 2, c, d + 1) [ d >= b + 1 /\ 5 >= b /\ 6*d >= 5*a + c + 7 /\ 5*d + b >= 5*a + c + 7 /\ d >= a + 1 /\ 29 >= a /\ b + 203 >= 2*d + 5*a + c /\ 2*b + 1561 >= 14*d + 35*a + 7*c /\ 140*d + 23*b >= 140*a + 28*c + 161 /\ 23*b + 5719 >= 56*d + 140*a + 28*c /\ d + 5 >= b /\ 7*d + c >= b + 7*a ]
		(1, 1)                    start0(a, b, c, d) -> start(a, c, c, a)
	start location:	start0
	leaf cost:	2

A polynomial rank function with
	Pol(start) = -13*V_1 - V_2 + V_3 + 354
	Pol(lbl171) = -7*V_1 - V_2 + V_3 - 6*V_4 + 354
	Pol(lbl151) = -7*V_1 - V_2 + V_3 - 6*V_4 + 362
	Pol(start0) = -13*V_1 + 354
orients all transitions weakly and the transition
	lbl171(a, b, c, d) -> lbl171(a, b - 10, c, d + 2) [ b >= d /\ 29 >= d /\ 29 >= a /\ 5*d + b >= 5*a + c /\ 7*d + c >= b + 7*a + 24 /\ 7*b + 1674 >= 19*d + 35*a + 7*c /\ b + 12 >= d ]
strictly and produces the following problem:
5:	T:
		(1, 1)                    start(a, b, c, d) -> lbl171(a, b - 10, c, d + 2) [ c >= a /\ 29 >= a /\ b = c /\ d = a ]
		(1, 1)                    start(a, b, c, d) -> lbl151(a, b + 7, c, d + 1) [ a >= c + 1 /\ c >= 6 /\ 29 >= a /\ b = c /\ d = a ]
		(1, 1)                    start(a, b, c, d) -> lbl151(a, b + 2, c, d + 1) [ a >= c + 1 /\ 5 >= c /\ 29 >= a /\ b = c /\ d = a ]
		(13*a + 354, 1)           lbl171(a, b, c, d) -> lbl171(a, b - 10, c, d + 2) [ b >= d /\ 29 >= d /\ 29 >= a /\ 5*d + b >= 5*a + c /\ 7*d + c >= b + 7*a + 24 /\ 7*b + 1674 >= 19*d + 35*a + 7*c /\ b + 12 >= d ]
		(47*a + 9*c + 1720, 1)    lbl171(a, b, c, d) -> lbl151(a, b + 7, c, d + 1) [ d >= b + 1 /\ b >= 6 /\ 29 >= d /\ 29 >= a /\ 5*d + b >= 5*a + c /\ 7*d + c >= b + 7*a + 24 /\ 7*b + 1674 >= 19*d + 35*a + 7*c /\ b + 12 >= d ]
		(47*a + 9*c + 1720, 1)    lbl171(a, b, c, d) -> lbl151(a, b + 2, c, d + 1) [ d >= b + 1 /\ 5 >= b /\ 29 >= d /\ 29 >= a /\ 5*d + b >= 5*a + c /\ 7*d + c >= b + 7*a + 24 /\ 7*b + 1674 >= 19*d + 35*a + 7*c /\ b + 12 >= d ]
		(47*a + 9*c + 1720, 1)    lbl151(a, b, c, d) -> lbl171(a, b - 10, c, d + 2) [ b >= d /\ 6*d >= 5*a + c + 7 /\ 5*d + b >= 5*a + c + 7 /\ d >= a + 1 /\ 29 >= a /\ b + 203 >= 2*d + 5*a + c /\ 2*b + 1561 >= 14*d + 35*a + 7*c /\ 140*d + 23*b >= 140*a + 28*c + 161 /\ 23*b + 5719 >= 56*d + 140*a + 28*c /\ d + 5 >= b /\ 7*d + c >= b + 7*a ]
		(47*a + 9*c + 1720, 1)    lbl151(a, b, c, d) -> lbl151(a, b + 7, c, d + 1) [ d >= b + 1 /\ b >= 6 /\ 6*d >= 5*a + c + 7 /\ 5*d + b >= 5*a + c + 7 /\ d >= a + 1 /\ 29 >= a /\ b + 203 >= 2*d + 5*a + c /\ 2*b + 1561 >= 14*d + 35*a + 7*c /\ 140*d + 23*b >= 140*a + 28*c + 161 /\ 23*b + 5719 >= 56*d + 140*a + 28*c /\ d + 5 >= b /\ 7*d + c >= b + 7*a ]
		(47*a + 9*c + 1720, 1)    lbl151(a, b, c, d) -> lbl151(a, b + 2, c, d + 1) [ d >= b + 1 /\ 5 >= b /\ 6*d >= 5*a + c + 7 /\ 5*d + b >= 5*a + c + 7 /\ d >= a + 1 /\ 29 >= a /\ b + 203 >= 2*d + 5*a + c /\ 2*b + 1561 >= 14*d + 35*a + 7*c /\ 140*d + 23*b >= 140*a + 28*c + 161 /\ 23*b + 5719 >= 56*d + 140*a + 28*c /\ d + 5 >= b /\ 7*d + c >= b + 7*a ]
		(1, 1)                    start0(a, b, c, d) -> start(a, c, c, a)
	start location:	start0
	leaf cost:	2

Complexity upper bound 248*a + 45*c + 8960

Time: 1.197 sec (SMT: 1.148 sec)