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

Initial complexity problem:
1:	T:
		(?, 1)    start(a, b, c, d, e, f, g, h) -> stop(a, b, c, d, e, f, g, h) [ 1 >= a /\ b = c /\ d = e /\ f = g /\ h = a ]
		(?, 1)    start(a, b, c, d, e, f, g, h) -> lbl111(a, h, c, 1, e, h - 1, g, h) [ a >= 2 /\ b = c /\ d = e /\ f = g /\ h = a ]
		(?, 1)    lbl16(a, b, c, d, e, f, g, h) -> stop(a, b, c, d, e, f, g, h) [ a >= 2 /\ a >= b + 1 /\ f = 0 /\ h = a /\ d = a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ d >= f /\ a >= f + 1 /\ a >= f + d /\ a >= b /\ f >= 1 /\ d >= 0 /\ h = a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, h, e, f - 1, g, h) [ f >= d + 1 /\ 0 >= d + 1 /\ a >= f + 1 /\ a >= f + d /\ a >= b /\ f >= 1 /\ d >= 0 /\ h = a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, h, e, f - 1, g, h) [ f >= d + 1 /\ d >= 1 /\ a >= f + 1 /\ a >= f + d /\ a >= b /\ f >= 1 /\ d >= 0 /\ h = a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b - f, c, h, e, f - 1, g, h) [ f >= 1 /\ a >= f + 1 /\ a >= f /\ a >= b /\ d = 0 /\ h = a ]
		(?, 1)    lbl82(a, b, c, d, e, f, g, h) -> lbl16(a, b, c, d, e, f, g, h) [ a >= 2 /\ a >= b /\ a >= b + 1 /\ f = 0 /\ h = a /\ d = a ]
		(?, 1)    lbl82(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ f >= 1 /\ a >= f /\ f >= 0 /\ a >= f + 2 /\ a >= b /\ a + f >= b + 1 /\ h = a /\ d = a ]
		(?, 1)    lbl82(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, h, e, f - 1, g, h) [ f >= a + 1 /\ a >= 1 /\ f >= 0 /\ a >= f + 2 /\ a >= b /\ a + f >= b + 1 /\ h = a /\ d = a ]
		(?, 1)    lbl82(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, h, e, f - 1, g, h) [ f >= 1 /\ 0 >= a + 1 /\ f >= 0 /\ a >= f + 2 /\ a >= b /\ a + f >= b + 1 /\ h = a /\ d = a ]
		(?, 1)    lbl82(a, b, c, d, e, f, g, h) -> lbl82(a, b - f, c, h, e, f - 1, g, h) [ f >= 1 /\ f >= 0 /\ 0 >= f + 2 /\ 0 >= b /\ f >= b + 1 /\ d = 0 /\ h = 0 /\ a = 0 ]
		(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:
	lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, h, e, f - 1, g, h) [ f >= d + 1 /\ 0 >= d + 1 /\ a >= f + 1 /\ a >= f + d /\ a >= b /\ f >= 1 /\ d >= 0 /\ h = a ]
	lbl82(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, h, e, f - 1, g, h) [ f >= a + 1 /\ a >= 1 /\ f >= 0 /\ a >= f + 2 /\ a >= b /\ a + f >= b + 1 /\ h = a /\ d = a ]
	lbl82(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, h, e, f - 1, g, h) [ f >= 1 /\ 0 >= a + 1 /\ f >= 0 /\ a >= f + 2 /\ a >= b /\ a + f >= b + 1 /\ h = a /\ d = a ]
	lbl82(a, b, c, d, e, f, g, h) -> lbl82(a, b - f, c, h, e, f - 1, g, h) [ f >= 1 /\ f >= 0 /\ 0 >= f + 2 /\ 0 >= b /\ f >= b + 1 /\ d = 0 /\ h = 0 /\ a = 0 ]
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) [ 1 >= a /\ b = c /\ d = e /\ f = g /\ h = a ]
		(?, 1)    start(a, b, c, d, e, f, g, h) -> lbl111(a, h, c, 1, e, h - 1, g, h) [ a >= 2 /\ b = c /\ d = e /\ f = g /\ h = a ]
		(?, 1)    lbl16(a, b, c, d, e, f, g, h) -> stop(a, b, c, d, e, f, g, h) [ a >= 2 /\ a >= b + 1 /\ f = 0 /\ h = a /\ d = a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ d >= f /\ a >= f + 1 /\ a >= f + d /\ a >= b /\ f >= 1 /\ d >= 0 /\ h = a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, h, e, f - 1, g, h) [ f >= d + 1 /\ d >= 1 /\ a >= f + 1 /\ a >= f + d /\ a >= b /\ f >= 1 /\ d >= 0 /\ h = a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b - f, c, h, e, f - 1, g, h) [ f >= 1 /\ a >= f + 1 /\ a >= f /\ a >= b /\ d = 0 /\ h = a ]
		(?, 1)    lbl82(a, b, c, d, e, f, g, h) -> lbl16(a, b, c, d, e, f, g, h) [ a >= 2 /\ a >= b /\ a >= b + 1 /\ f = 0 /\ h = a /\ d = a ]
		(?, 1)    lbl82(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ f >= 1 /\ a >= f /\ f >= 0 /\ a >= f + 2 /\ a >= b /\ a + f >= b + 1 /\ h = a /\ d = a ]
		(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) -> lbl111(a, h, c, 1, e, h - 1, g, h) [ a >= 2 /\ b = c /\ d = e /\ f = g /\ h = a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ d >= f /\ a >= f + 1 /\ a >= f + d /\ a >= b /\ f >= 1 /\ d >= 0 /\ h = a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, h, e, f - 1, g, h) [ f >= d + 1 /\ d >= 1 /\ a >= f + 1 /\ a >= f + d /\ a >= b /\ f >= 1 /\ d >= 0 /\ h = a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b - f, c, h, e, f - 1, g, h) [ f >= 1 /\ a >= f + 1 /\ a >= f /\ a >= b /\ d = 0 /\ h = a ]
		(?, 1)    lbl82(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ f >= 1 /\ a >= f /\ f >= 0 /\ a >= f + 2 /\ a >= b /\ a + f >= b + 1 /\ h = a /\ d = a ]
		(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:	3

Repeatedly propagating knowledge in problem 3 produces the following problem:
4:	T:
		(1, 1)    start(a, b, c, d, e, f, g, h) -> lbl111(a, h, c, 1, e, h - 1, g, h) [ a >= 2 /\ b = c /\ d = e /\ f = g /\ h = a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ d >= f /\ a >= f + 1 /\ a >= f + d /\ a >= b /\ f >= 1 /\ d >= 0 /\ h = a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, h, e, f - 1, g, h) [ f >= d + 1 /\ d >= 1 /\ a >= f + 1 /\ a >= f + d /\ a >= b /\ f >= 1 /\ d >= 0 /\ h = a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b - f, c, h, e, f - 1, g, h) [ f >= 1 /\ a >= f + 1 /\ a >= f /\ a >= b /\ d = 0 /\ h = a ]
		(?, 1)    lbl82(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ f >= 1 /\ a >= f /\ f >= 0 /\ a >= f + 2 /\ a >= b /\ a + f >= b + 1 /\ h = a /\ d = a ]
		(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:	3

A polynomial rank function with
	Pol(start) = 2*V_8 - 2
	Pol(lbl111) = 2*V_6
	Pol(lbl82) = 2*V_6 + 1
	Pol(start0) = 2*V_1 - 2
orients all transitions weakly and the transitions
	lbl82(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ f >= 1 /\ a >= f /\ f >= 0 /\ a >= f + 2 /\ a >= b /\ a + f >= b + 1 /\ h = a /\ d = a ]
	lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b - f, c, h, e, f - 1, g, h) [ f >= 1 /\ a >= f + 1 /\ a >= f /\ a >= b /\ d = 0 /\ h = a ]
	lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, h, e, f - 1, g, h) [ f >= d + 1 /\ d >= 1 /\ a >= f + 1 /\ a >= f + d /\ a >= b /\ f >= 1 /\ d >= 0 /\ h = a ]
strictly and produces the following problem:
5:	T:
		(1, 1)          start(a, b, c, d, e, f, g, h) -> lbl111(a, h, c, 1, e, h - 1, g, h) [ a >= 2 /\ b = c /\ d = e /\ f = g /\ h = a ]
		(?, 1)          lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ d >= f /\ a >= f + 1 /\ a >= f + d /\ a >= b /\ f >= 1 /\ d >= 0 /\ h = a ]
		(2*a + 2, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, h, e, f - 1, g, h) [ f >= d + 1 /\ d >= 1 /\ a >= f + 1 /\ a >= f + d /\ a >= b /\ f >= 1 /\ d >= 0 /\ h = a ]
		(2*a + 2, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b - f, c, h, e, f - 1, g, h) [ f >= 1 /\ a >= f + 1 /\ a >= f /\ a >= b /\ d = 0 /\ h = a ]
		(2*a + 2, 1)    lbl82(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ f >= 1 /\ a >= f /\ f >= 0 /\ a >= f + 2 /\ a >= b /\ a + f >= b + 1 /\ h = a /\ d = a ]
		(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:	3

A polynomial rank function with
	Pol(lbl111) = V_4 + 1
and size complexities
	S("start0(a, b, c, d, e, f, g, h) -> start(a, c, c, e, e, g, g, a)", 0-0) = a
	S("start0(a, b, c, d, e, f, g, h) -> start(a, c, c, e, e, g, g, a)", 0-1) = c
	S("start0(a, b, c, d, e, f, g, h) -> start(a, c, c, e, e, g, g, a)", 0-2) = c
	S("start0(a, b, c, d, e, f, g, h) -> start(a, c, c, e, e, g, g, a)", 0-3) = e
	S("start0(a, b, c, d, e, f, g, h) -> start(a, c, c, e, e, g, g, a)", 0-4) = e
	S("start0(a, b, c, d, e, f, g, h) -> start(a, c, c, e, e, g, g, a)", 0-5) = g
	S("start0(a, b, c, d, e, f, g, h) -> start(a, c, c, e, e, g, g, a)", 0-6) = g
	S("start0(a, b, c, d, e, f, g, h) -> start(a, c, c, e, e, g, g, a)", 0-7) = a
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ f >= 1 /\\ a >= f /\\ f >= 0 /\\ a >= f + 2 /\\ a >= b /\\ a + f >= b + 1 /\\ h = a /\\ d = a ]", 0-0) = a
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ f >= 1 /\\ a >= f /\\ f >= 0 /\\ a >= f + 2 /\\ a >= b /\\ a + f >= b + 1 /\\ h = a /\\ d = a ]", 0-1) = 3*a + 2*a^2
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ f >= 1 /\\ a >= f /\\ f >= 0 /\\ a >= f + 2 /\\ a >= b /\\ a + f >= b + 1 /\\ h = a /\\ d = a ]", 0-2) = c
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ f >= 1 /\\ a >= f /\\ f >= 0 /\\ a >= f + 2 /\\ a >= b /\\ a + f >= b + 1 /\\ h = a /\\ d = a ]", 0-3) = a
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ f >= 1 /\\ a >= f /\\ f >= 0 /\\ a >= f + 2 /\\ a >= b /\\ a + f >= b + 1 /\\ h = a /\\ d = a ]", 0-4) = e
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ f >= 1 /\\ a >= f /\\ f >= 0 /\\ a >= f + 2 /\\ a >= b /\\ a + f >= b + 1 /\\ h = a /\\ d = a ]", 0-5) = a
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ f >= 1 /\\ a >= f /\\ f >= 0 /\\ a >= f + 2 /\\ a >= b /\\ a + f >= b + 1 /\\ h = a /\\ d = a ]", 0-6) = g
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ f >= 1 /\\ a >= f /\\ f >= 0 /\\ a >= f + 2 /\\ a >= b /\\ a + f >= b + 1 /\\ h = a /\\ d = a ]", 0-7) = a
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b - f, c, h, e, f - 1, g, h) [ f >= 1 /\\ a >= f + 1 /\\ a >= f /\\ a >= b /\\ d = 0 /\\ h = a ]", 0-0) = a
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b - f, c, h, e, f - 1, g, h) [ f >= 1 /\\ a >= f + 1 /\\ a >= f /\\ a >= b /\\ d = 0 /\\ h = a ]", 0-1) = 3*a + 2*a^2
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b - f, c, h, e, f - 1, g, h) [ f >= 1 /\\ a >= f + 1 /\\ a >= f /\\ a >= b /\\ d = 0 /\\ h = a ]", 0-2) = c
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b - f, c, h, e, f - 1, g, h) [ f >= 1 /\\ a >= f + 1 /\\ a >= f /\\ a >= b /\\ d = 0 /\\ h = a ]", 0-3) = a
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b - f, c, h, e, f - 1, g, h) [ f >= 1 /\\ a >= f + 1 /\\ a >= f /\\ a >= b /\\ d = 0 /\\ h = a ]", 0-4) = e
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b - f, c, h, e, f - 1, g, h) [ f >= 1 /\\ a >= f + 1 /\\ a >= f /\\ a >= b /\\ d = 0 /\\ h = a ]", 0-5) = a
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b - f, c, h, e, f - 1, g, h) [ f >= 1 /\\ a >= f + 1 /\\ a >= f /\\ a >= b /\\ d = 0 /\\ h = a ]", 0-6) = g
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b - f, c, h, e, f - 1, g, h) [ f >= 1 /\\ a >= f + 1 /\\ a >= f /\\ a >= b /\\ d = 0 /\\ h = a ]", 0-7) = a
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, h, e, f - 1, g, h) [ f >= d + 1 /\\ d >= 1 /\\ a >= f + 1 /\\ a >= f + d /\\ a >= b /\\ f >= 1 /\\ d >= 0 /\\ h = a ]", 0-0) = a
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, h, e, f - 1, g, h) [ f >= d + 1 /\\ d >= 1 /\\ a >= f + 1 /\\ a >= f + d /\\ a >= b /\\ f >= 1 /\\ d >= 0 /\\ h = a ]", 0-1) = 3*a + 2*a^2
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, h, e, f - 1, g, h) [ f >= d + 1 /\\ d >= 1 /\\ a >= f + 1 /\\ a >= f + d /\\ a >= b /\\ f >= 1 /\\ d >= 0 /\\ h = a ]", 0-2) = c
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, h, e, f - 1, g, h) [ f >= d + 1 /\\ d >= 1 /\\ a >= f + 1 /\\ a >= f + d /\\ a >= b /\\ f >= 1 /\\ d >= 0 /\\ h = a ]", 0-3) = a
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, h, e, f - 1, g, h) [ f >= d + 1 /\\ d >= 1 /\\ a >= f + 1 /\\ a >= f + d /\\ a >= b /\\ f >= 1 /\\ d >= 0 /\\ h = a ]", 0-4) = e
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, h, e, f - 1, g, h) [ f >= d + 1 /\\ d >= 1 /\\ a >= f + 1 /\\ a >= f + d /\\ a >= b /\\ f >= 1 /\\ d >= 0 /\\ h = a ]", 0-5) = a
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, h, e, f - 1, g, h) [ f >= d + 1 /\\ d >= 1 /\\ a >= f + 1 /\\ a >= f + d /\\ a >= b /\\ f >= 1 /\\ d >= 0 /\\ h = a ]", 0-6) = g
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, h, e, f - 1, g, h) [ f >= d + 1 /\\ d >= 1 /\\ a >= f + 1 /\\ a >= f + d /\\ a >= b /\\ f >= 1 /\\ d >= 0 /\\ h = a ]", 0-7) = a
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ d >= f /\\ a >= f + 1 /\\ a >= f + d /\\ a >= b /\\ f >= 1 /\\ d >= 0 /\\ h = a ]", 0-0) = a
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ d >= f /\\ a >= f + 1 /\\ a >= f + d /\\ a >= b /\\ f >= 1 /\\ d >= 0 /\\ h = a ]", 0-1) = 3*a + 2*a^2
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ d >= f /\\ a >= f + 1 /\\ a >= f + d /\\ a >= b /\\ f >= 1 /\\ d >= 0 /\\ h = a ]", 0-2) = c
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ d >= f /\\ a >= f + 1 /\\ a >= f + d /\\ a >= b /\\ f >= 1 /\\ d >= 0 /\\ h = a ]", 0-3) = a + 1
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ d >= f /\\ a >= f + 1 /\\ a >= f + d /\\ a >= b /\\ f >= 1 /\\ d >= 0 /\\ h = a ]", 0-4) = e
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ d >= f /\\ a >= f + 1 /\\ a >= f + d /\\ a >= b /\\ f >= 1 /\\ d >= 0 /\\ h = a ]", 0-5) = a
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ d >= f /\\ a >= f + 1 /\\ a >= f + d /\\ a >= b /\\ f >= 1 /\\ d >= 0 /\\ h = a ]", 0-6) = g
	S("lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ d >= f /\\ a >= f + 1 /\\ a >= f + d /\\ a >= b /\\ f >= 1 /\\ d >= 0 /\\ h = a ]", 0-7) = a
	S("start(a, b, c, d, e, f, g, h) -> lbl111(a, h, c, 1, e, h - 1, g, h) [ a >= 2 /\\ b = c /\\ d = e /\\ f = g /\\ h = a ]", 0-0) = a
	S("start(a, b, c, d, e, f, g, h) -> lbl111(a, h, c, 1, e, h - 1, g, h) [ a >= 2 /\\ b = c /\\ d = e /\\ f = g /\\ h = a ]", 0-1) = a
	S("start(a, b, c, d, e, f, g, h) -> lbl111(a, h, c, 1, e, h - 1, g, h) [ a >= 2 /\\ b = c /\\ d = e /\\ f = g /\\ h = a ]", 0-2) = c
	S("start(a, b, c, d, e, f, g, h) -> lbl111(a, h, c, 1, e, h - 1, g, h) [ a >= 2 /\\ b = c /\\ d = e /\\ f = g /\\ h = a ]", 0-3) = 1
	S("start(a, b, c, d, e, f, g, h) -> lbl111(a, h, c, 1, e, h - 1, g, h) [ a >= 2 /\\ b = c /\\ d = e /\\ f = g /\\ h = a ]", 0-4) = e
	S("start(a, b, c, d, e, f, g, h) -> lbl111(a, h, c, 1, e, h - 1, g, h) [ a >= 2 /\\ b = c /\\ d = e /\\ f = g /\\ h = a ]", 0-5) = a
	S("start(a, b, c, d, e, f, g, h) -> lbl111(a, h, c, 1, e, h - 1, g, h) [ a >= 2 /\\ b = c /\\ d = e /\\ f = g /\\ h = a ]", 0-6) = g
	S("start(a, b, c, d, e, f, g, h) -> lbl111(a, h, c, 1, e, h - 1, g, h) [ a >= 2 /\\ b = c /\\ d = e /\\ f = g /\\ h = a ]", 0-7) = a
orients the transition
	lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ d >= f /\ a >= f + 1 /\ a >= f + d /\ a >= b /\ f >= 1 /\ d >= 0 /\ h = a ]
weakly and the transition
	lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ d >= f /\ a >= f + 1 /\ a >= f + d /\ a >= b /\ f >= 1 /\ d >= 0 /\ h = a ]
strictly and produces the following problem:
6:	T:
		(1, 1)                  start(a, b, c, d, e, f, g, h) -> lbl111(a, h, c, 1, e, h - 1, g, h) [ a >= 2 /\ b = c /\ d = e /\ f = g /\ h = a ]
		(2*a^2 + 4*a + 4, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ d >= f /\ a >= f + 1 /\ a >= f + d /\ a >= b /\ f >= 1 /\ d >= 0 /\ h = a ]
		(2*a + 2, 1)            lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, h, e, f - 1, g, h) [ f >= d + 1 /\ d >= 1 /\ a >= f + 1 /\ a >= f + d /\ a >= b /\ f >= 1 /\ d >= 0 /\ h = a ]
		(2*a + 2, 1)            lbl111(a, b, c, d, e, f, g, h) -> lbl82(a, b - f, c, h, e, f - 1, g, h) [ f >= 1 /\ a >= f + 1 /\ a >= f /\ a >= b /\ d = 0 /\ h = a ]
		(2*a + 2, 1)            lbl82(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d - f, e, f, g, h) [ f >= 1 /\ a >= f /\ f >= 0 /\ a >= f + 2 /\ a >= b /\ a + f >= b + 1 /\ h = a /\ d = a ]
		(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:	3

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

Time: 0.651 sec (SMT: 0.611 sec)