YES(?, 6*g + 9)

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

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

A polynomial rank function with
	Pol(start) = 2*V_6 - 1
	Pol(lM1) = 2*V_4 + 1
	Pol(lZZ1) = 2*V_4
	Pol(start0) = 2*V_7 - 1
orients all transitions weakly and the transitions
	lZZ1(a, b, c, d, e, f, g, h) -> lM1(a, b + 1, c, d - 1, e, f, g, h) [ a >= 1 /\ d >= 1 /\ g >= a + d /\ a >= 2 /\ b = 0 /\ h = a /\ f = g ]
	lM1(a, b, c, d, e, f, g, h) -> lZZ1(a, 0, c, d, e, f, g, h) [ d >= 1 /\ g >= d + a /\ a >= 1 /\ d >= 0 /\ b = a /\ h = a /\ f = g ]
	lM1(a, b, c, d, e, f, g, h) -> lM1(a, b + 1, c, d - 1, e, f, g, h) [ a >= b + 1 /\ d >= 1 /\ a >= b /\ g >= d + b /\ b >= 1 /\ d >= 0 /\ h = a /\ f = g ]
strictly and produces the following problem:
5:	T:
		(1, 1)          start(a, b, c, d, e, f, g, h) -> lM1(a, 1, c, f - 1, e, f, g, h) [ a >= 1 /\ g >= 1 /\ b = c /\ d = e /\ f = g /\ h = a ]
		(2*g + 1, 1)    lM1(a, b, c, d, e, f, g, h) -> lZZ1(a, 0, c, d, e, f, g, h) [ d >= 1 /\ g >= d + a /\ a >= 1 /\ d >= 0 /\ b = a /\ h = a /\ f = g ]
		(2*g + 1, 1)    lM1(a, b, c, d, e, f, g, h) -> lM1(a, b + 1, c, d - 1, e, f, g, h) [ a >= b + 1 /\ d >= 1 /\ a >= b /\ g >= d + b /\ b >= 1 /\ d >= 0 /\ h = a /\ f = g ]
		(2*g + 1, 1)    lZZ1(a, b, c, d, e, f, g, h) -> lM1(a, b + 1, c, d - 1, e, f, g, h) [ a >= 1 /\ d >= 1 /\ g >= a + d /\ a >= 2 /\ b = 0 /\ h = a /\ f = g ]
		(1, 1)          start0(a, b, c, d, e, f, g, h) -> start(a, c, c, e, e, g, g, a)
	start location:	start0
	leaf cost:	4

Complexity upper bound 6*g + 9

Time: 0.420 sec (SMT: 0.398 sec)