YES(?, 6*a^2 + 43*a + 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 + 1 /\ b = c /\ d = a /\ e = f /\ g = h ]
		(?, 1)    start(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, 2*d, f, 2*d - 1, h) [ a >= 0 /\ b = c /\ d = a /\ e = f /\ g = h ]
		(?, 1)    start(a, b, c, d, e, f, g, h) -> lbl121(a, 2*d, c, d, 2*d - 1, f, 2*d - 1, h) [ a >= 0 /\ b = c /\ d = a /\ e = f /\ g = h ]
		(?, 1)    lbl82(a, b, c, d, e, f, g, h) -> stop(a, b, c, d, e, f, g, h) [ e >= a /\ 2*a >= e /\ d = a /\ g + 1 = a ]
		(?, 1)    lbl82(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ g >= a /\ e >= g + 1 /\ 2*a >= e /\ g + 1 >= a /\ d = a ]
		(?, 1)    lbl82(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ g >= a /\ e >= g + 1 /\ 2*a >= e /\ g + 1 >= a /\ d = a ]
		(?, 1)    lbl121(a, b, c, d, e, f, g, h) -> stop(a, b, c, d, e, f, g, h) [ a >= e + 1 /\ 2*a >= e + 1 /\ b >= a /\ e + 1 >= b /\ g = e /\ d = a ]
		(?, 1)    lbl121(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ e >= a /\ 2*a >= e + 1 /\ b >= a /\ e + 1 >= b /\ g = e /\ d = a ]
		(?, 1)    lbl121(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ e >= a /\ 2*a >= e + 1 /\ b >= a /\ e + 1 >= b /\ g = e /\ d = a ]
		(1, 1)    start0(a, b, c, d, e, f, g, h) -> start(a, c, c, a, f, f, h, h)
	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, e, f, g, h) -> lbl82(a, b, c, d, 2*d, f, 2*d - 1, h) [ a >= 0 /\ b = c /\ d = a /\ e = f /\ g = h ]
		(?, 1)    start(a, b, c, d, e, f, g, h) -> lbl121(a, 2*d, c, d, 2*d - 1, f, 2*d - 1, h) [ a >= 0 /\ b = c /\ d = a /\ e = f /\ g = h ]
		(?, 1)    lbl82(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ g >= a /\ e >= g + 1 /\ 2*a >= e /\ g + 1 >= a /\ d = a ]
		(?, 1)    lbl82(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ g >= a /\ e >= g + 1 /\ 2*a >= e /\ g + 1 >= a /\ d = a ]
		(?, 1)    lbl121(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ e >= a /\ 2*a >= e + 1 /\ b >= a /\ e + 1 >= b /\ g = e /\ d = a ]
		(?, 1)    lbl121(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ e >= a /\ 2*a >= e + 1 /\ b >= a /\ e + 1 >= b /\ g = e /\ d = a ]
		(1, 1)    start0(a, b, c, d, e, f, g, h) -> start(a, c, c, a, f, f, h, h)
	start location:	start0
	leaf cost:	3

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(1, 1)    start(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, 2*d, f, 2*d - 1, h) [ a >= 0 /\ b = c /\ d = a /\ e = f /\ g = h ]
		(1, 1)    start(a, b, c, d, e, f, g, h) -> lbl121(a, 2*d, c, d, 2*d - 1, f, 2*d - 1, h) [ a >= 0 /\ b = c /\ d = a /\ e = f /\ g = h ]
		(?, 1)    lbl82(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ g >= a /\ e >= g + 1 /\ 2*a >= e /\ g + 1 >= a /\ d = a ]
		(?, 1)    lbl82(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ g >= a /\ e >= g + 1 /\ 2*a >= e /\ g + 1 >= a /\ d = a ]
		(?, 1)    lbl121(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ e >= a /\ 2*a >= e + 1 /\ b >= a /\ e + 1 >= b /\ g = e /\ d = a ]
		(?, 1)    lbl121(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ e >= a /\ 2*a >= e + 1 /\ b >= a /\ e + 1 >= b /\ g = e /\ d = a ]
		(1, 1)    start0(a, b, c, d, e, f, g, h) -> start(a, c, c, a, f, f, h, h)
	start location:	start0
	leaf cost:	3

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

A polynomial rank function with
	Pol(lbl82) = -V_1 + V_7 + 1
and size complexities
	S("start0(a, b, c, d, e, f, g, h) -> start(a, c, c, a, f, f, h, h)", 0-0) = a
	S("start0(a, b, c, d, e, f, g, h) -> start(a, c, c, a, f, f, h, h)", 0-1) = c
	S("start0(a, b, c, d, e, f, g, h) -> start(a, c, c, a, f, f, h, h)", 0-2) = c
	S("start0(a, b, c, d, e, f, g, h) -> start(a, c, c, a, f, f, h, h)", 0-3) = a
	S("start0(a, b, c, d, e, f, g, h) -> start(a, c, c, a, f, f, h, h)", 0-4) = f
	S("start0(a, b, c, d, e, f, g, h) -> start(a, c, c, a, f, f, h, h)", 0-5) = f
	S("start0(a, b, c, d, e, f, g, h) -> start(a, c, c, a, f, f, h, h)", 0-6) = h
	S("start0(a, b, c, d, e, f, g, h) -> start(a, c, c, a, f, f, h, h)", 0-7) = h
	S("lbl121(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ e >= a /\\ 2*a >= e + 1 /\\ b >= a /\\ e + 1 >= b /\\ g = e /\\ d = a ]", 0-0) = a
	S("lbl121(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ e >= a /\\ 2*a >= e + 1 /\\ b >= a /\\ e + 1 >= b /\\ g = e /\\ d = a ]", 0-1) = 2*a + 16
	S("lbl121(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ e >= a /\\ 2*a >= e + 1 /\\ b >= a /\\ e + 1 >= b /\\ g = e /\\ d = a ]", 0-2) = c
	S("lbl121(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ e >= a /\\ 2*a >= e + 1 /\\ b >= a /\\ e + 1 >= b /\\ g = e /\\ d = a ]", 0-3) = a
	S("lbl121(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ e >= a /\\ 2*a >= e + 1 /\\ b >= a /\\ e + 1 >= b /\\ g = e /\\ d = a ]", 0-4) = 2*a + 4
	S("lbl121(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ e >= a /\\ 2*a >= e + 1 /\\ b >= a /\\ e + 1 >= b /\\ g = e /\\ d = a ]", 0-5) = f
	S("lbl121(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ e >= a /\\ 2*a >= e + 1 /\\ b >= a /\\ e + 1 >= b /\\ g = e /\\ d = a ]", 0-6) = 2*a + 8
	S("lbl121(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ e >= a /\\ 2*a >= e + 1 /\\ b >= a /\\ e + 1 >= b /\\ g = e /\\ d = a ]", 0-7) = h
	S("lbl121(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ e >= a /\\ 2*a >= e + 1 /\\ b >= a /\\ e + 1 >= b /\\ g = e /\\ d = a ]", 0-0) = a
	S("lbl121(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ e >= a /\\ 2*a >= e + 1 /\\ b >= a /\\ e + 1 >= b /\\ g = e /\\ d = a ]", 0-1) = 2*a + 128
	S("lbl121(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ e >= a /\\ 2*a >= e + 1 /\\ b >= a /\\ e + 1 >= b /\\ g = e /\\ d = a ]", 0-2) = c
	S("lbl121(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ e >= a /\\ 2*a >= e + 1 /\\ b >= a /\\ e + 1 >= b /\\ g = e /\\ d = a ]", 0-3) = a
	S("lbl121(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ e >= a /\\ 2*a >= e + 1 /\\ b >= a /\\ e + 1 >= b /\\ g = e /\\ d = a ]", 0-4) = 2*a + 4
	S("lbl121(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ e >= a /\\ 2*a >= e + 1 /\\ b >= a /\\ e + 1 >= b /\\ g = e /\\ d = a ]", 0-5) = f
	S("lbl121(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ e >= a /\\ 2*a >= e + 1 /\\ b >= a /\\ e + 1 >= b /\\ g = e /\\ d = a ]", 0-6) = 2*a + 16
	S("lbl121(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ e >= a /\\ 2*a >= e + 1 /\\ b >= a /\\ e + 1 >= b /\\ g = e /\\ d = a ]", 0-7) = h
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ g >= a /\\ e >= g + 1 /\\ 2*a >= e /\\ g + 1 >= a /\\ d = a ]", 0-0) = a
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ g >= a /\\ e >= g + 1 /\\ 2*a >= e /\\ g + 1 >= a /\\ d = a ]", 0-1) = 2*a + 64
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ g >= a /\\ e >= g + 1 /\\ 2*a >= e /\\ g + 1 >= a /\\ d = a ]", 0-2) = c
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ g >= a /\\ e >= g + 1 /\\ 2*a >= e /\\ g + 1 >= a /\\ d = a ]", 0-3) = a
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ g >= a /\\ e >= g + 1 /\\ 2*a >= e /\\ g + 1 >= a /\\ d = a ]", 0-4) = 2*a + 4
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ g >= a /\\ e >= g + 1 /\\ 2*a >= e /\\ g + 1 >= a /\\ d = a ]", 0-5) = f
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ g >= a /\\ e >= g + 1 /\\ 2*a >= e /\\ g + 1 >= a /\\ d = a ]", 0-6) = 2*a + 8
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ g >= a /\\ e >= g + 1 /\\ 2*a >= e /\\ g + 1 >= a /\\ d = a ]", 0-7) = h
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ g >= a /\\ e >= g + 1 /\\ 2*a >= e /\\ g + 1 >= a /\\ d = a ]", 0-0) = a
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ g >= a /\\ e >= g + 1 /\\ 2*a >= e /\\ g + 1 >= a /\\ d = a ]", 0-1) = 2*a + 2*c + 256
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ g >= a /\\ e >= g + 1 /\\ 2*a >= e /\\ g + 1 >= a /\\ d = a ]", 0-2) = c
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ g >= a /\\ e >= g + 1 /\\ 2*a >= e /\\ g + 1 >= a /\\ d = a ]", 0-3) = a
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ g >= a /\\ e >= g + 1 /\\ 2*a >= e /\\ g + 1 >= a /\\ d = a ]", 0-4) = 2*a + 4
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ g >= a /\\ e >= g + 1 /\\ 2*a >= e /\\ g + 1 >= a /\\ d = a ]", 0-5) = f
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ g >= a /\\ e >= g + 1 /\\ 2*a >= e /\\ g + 1 >= a /\\ d = a ]", 0-6) = 2*a + 32
	S("lbl82(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ g >= a /\\ e >= g + 1 /\\ 2*a >= e /\\ g + 1 >= a /\\ d = a ]", 0-7) = h
	S("start(a, b, c, d, e, f, g, h) -> lbl121(a, 2*d, c, d, 2*d - 1, f, 2*d - 1, h) [ a >= 0 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-0) = a
	S("start(a, b, c, d, e, f, g, h) -> lbl121(a, 2*d, c, d, 2*d - 1, f, 2*d - 1, h) [ a >= 0 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-1) = 2*a
	S("start(a, b, c, d, e, f, g, h) -> lbl121(a, 2*d, c, d, 2*d - 1, f, 2*d - 1, h) [ a >= 0 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-2) = c
	S("start(a, b, c, d, e, f, g, h) -> lbl121(a, 2*d, c, d, 2*d - 1, f, 2*d - 1, h) [ a >= 0 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-3) = a
	S("start(a, b, c, d, e, f, g, h) -> lbl121(a, 2*d, c, d, 2*d - 1, f, 2*d - 1, h) [ a >= 0 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-4) = 2*a + 2
	S("start(a, b, c, d, e, f, g, h) -> lbl121(a, 2*d, c, d, 2*d - 1, f, 2*d - 1, h) [ a >= 0 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-5) = f
	S("start(a, b, c, d, e, f, g, h) -> lbl121(a, 2*d, c, d, 2*d - 1, f, 2*d - 1, h) [ a >= 0 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-6) = 2*a + 2
	S("start(a, b, c, d, e, f, g, h) -> lbl121(a, 2*d, c, d, 2*d - 1, f, 2*d - 1, h) [ a >= 0 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-7) = h
	S("start(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, 2*d, f, 2*d - 1, h) [ a >= 0 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-0) = a
	S("start(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, 2*d, f, 2*d - 1, h) [ a >= 0 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-1) = c
	S("start(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, 2*d, f, 2*d - 1, h) [ a >= 0 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-2) = c
	S("start(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, 2*d, f, 2*d - 1, h) [ a >= 0 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-3) = a
	S("start(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, 2*d, f, 2*d - 1, h) [ a >= 0 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-4) = 2*a
	S("start(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, 2*d, f, 2*d - 1, h) [ a >= 0 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-5) = f
	S("start(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, 2*d, f, 2*d - 1, h) [ a >= 0 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-6) = 2*a + 2
	S("start(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, 2*d, f, 2*d - 1, h) [ a >= 0 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-7) = h
orients the transition
	lbl82(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ g >= a /\ e >= g + 1 /\ 2*a >= e /\ g + 1 >= a /\ d = a ]
weakly and the transition
	lbl82(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ g >= a /\ e >= g + 1 /\ 2*a >= e /\ g + 1 >= a /\ d = a ]
strictly and produces the following problem:
5:	T:
		(1, 1)                   start(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, 2*d, f, 2*d - 1, h) [ a >= 0 /\ b = c /\ d = a /\ e = f /\ g = h ]
		(1, 1)                   start(a, b, c, d, e, f, g, h) -> lbl121(a, 2*d, c, d, 2*d - 1, f, 2*d - 1, h) [ a >= 0 /\ b = c /\ d = a /\ e = f /\ g = h ]
		(6*a^2 + 37*a + 3, 1)    lbl82(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ g >= a /\ e >= g + 1 /\ 2*a >= e /\ g + 1 >= a /\ d = a ]
		(2*a, 1)                 lbl82(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ g >= a /\ e >= g + 1 /\ 2*a >= e /\ g + 1 >= a /\ d = a ]
		(2*a, 1)                 lbl121(a, b, c, d, e, f, g, h) -> lbl82(a, b, c, d, e, f, g - 1, h) [ e >= a /\ 2*a >= e + 1 /\ b >= a /\ e + 1 >= b /\ g = e /\ d = a ]
		(2*a, 1)                 lbl121(a, b, c, d, e, f, g, h) -> lbl121(a, g, c, d, e - 1, f, e - 1, h) [ e >= a /\ 2*a >= e + 1 /\ b >= a /\ e + 1 >= b /\ g = e /\ d = a ]
		(1, 1)                   start0(a, b, c, d, e, f, g, h) -> start(a, c, c, a, f, f, h, h)
	start location:	start0
	leaf cost:	3

Complexity upper bound 6*a^2 + 43*a + 9

Time: 1.138 sec (SMT: 1.085 sec)