YES(?, 8*a + 813)

Initial complexity problem:
1:	T:
		(?, 1)    start(a, b, c, d, e, f, g, h) -> stop(a, h - 10, c, 1, e, h, g, h) [ a >= 101 /\ b = c /\ d = e /\ f = g /\ h = a ]
		(?, 1)    start(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, 2, e, h + 11, g, h) [ 100 >= a /\ b = c /\ d = e /\ f = g /\ h = a ]
		(?, 1)    lbl161(a, b, c, d, e, f, g, h) -> stop(a, b, c, d, e, f, g, h) [ 89 >= a /\ d = 1 /\ h = a /\ f = 101 /\ b = 91 ]
		(?, 1)    lbl161(a, b, c, d, e, f, g, h) -> lbl161(a, f - 20, c, d - 1, e, f - 10, g, h) [ 0 >= 10 /\ 89 >= a /\ 0 >= 1 /\ d = 2 /\ h = a /\ f = 101 /\ b = 91 ]
		(?, 1)    lbl161(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ 0 >= 2 /\ 89 >= a /\ h = a /\ f = 101 /\ d = 1 /\ b = 91 ]
		(?, 1)    lbl161(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ 0 >= 1 /\ 89 >= a /\ h = a /\ f = 101 /\ d = 1 /\ b = 91 ]
		(?, 1)    lbl161(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d - 1, e, f - 9, g, h) [ 0 >= 10 /\ 0 >= 2 /\ 89 >= a /\ h = a /\ f = 101 /\ d = 1 /\ b = 91 ]
		(?, 1)    lbl221(a, b, c, d, e, f, g, h) -> stop(a, b, c, d, e, f, g, h) [ 1 >= d /\ d >= 2 /\ f >= 102 /\ 111 >= f /\ f + 10 >= a + 11*d /\ 89 >= a /\ h = a /\ b = c ]
		(?, 1)    lbl221(a, b, c, d, e, f, g, h) -> lbl161(a, f - 20, c, d - 1, e, f - 10, g, h) [ 99 >= a /\ 89 >= a /\ f = 111 /\ d = 2 /\ h = a /\ b = c ]
		(?, 1)    lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ d >= 3 /\ 110 >= f /\ d >= 2 /\ f >= 102 /\ 111 >= f /\ f + 10 >= a + 11*d /\ 89 >= a /\ h = a /\ b = c ]
		(?, 1)    lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ d >= 2 /\ 110 >= f /\ f >= 102 /\ 111 >= f /\ f + 10 >= a + 11*d /\ 89 >= a /\ h = a /\ b = c ]
		(?, 1)    lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d - 1, e, f - 9, g, h) [ d >= 3 /\ d >= 2 /\ 121 >= a + 11*d /\ 89 >= a /\ f = 111 /\ h = a /\ b = c ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d + 1, e, f + 11, g, h) [ 111 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> stop(a, b, c, d, e, f, g, h) [ 11*d + a >= 112 /\ 1 >= d /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl161(a, f - 20, c, d - 1, e, f - 10, g, h) [ f = 111 /\ d = 2 /\ h = 100 /\ b = c /\ a = 100 ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ 11*d + a >= 112 /\ d >= 3 /\ 121 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ 11*d + a >= 112 /\ d >= 2 /\ 121 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d - 1, e, f - 9, g, h) [ d >= 3 /\ 11*d >= 22 /\ f = 111 /\ h + 11*d = 122 /\ b = c /\ a + 11*d = 122 ]
		(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:
	lbl161(a, b, c, d, e, f, g, h) -> lbl161(a, f - 20, c, d - 1, e, f - 10, g, h) [ 0 >= 10 /\ 89 >= a /\ 0 >= 1 /\ d = 2 /\ h = a /\ f = 101 /\ b = 91 ]
	lbl161(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ 0 >= 2 /\ 89 >= a /\ h = a /\ f = 101 /\ d = 1 /\ b = 91 ]
	lbl161(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ 0 >= 1 /\ 89 >= a /\ h = a /\ f = 101 /\ d = 1 /\ b = 91 ]
	lbl161(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d - 1, e, f - 9, g, h) [ 0 >= 10 /\ 0 >= 2 /\ 89 >= a /\ h = a /\ f = 101 /\ d = 1 /\ b = 91 ]
	lbl221(a, b, c, d, e, f, g, h) -> stop(a, b, c, d, e, f, g, h) [ 1 >= d /\ d >= 2 /\ f >= 102 /\ 111 >= f /\ f + 10 >= a + 11*d /\ 89 >= a /\ h = a /\ b = c ]
	lbl111(a, b, c, d, e, f, g, h) -> stop(a, b, c, d, e, f, g, h) [ 11*d + a >= 112 /\ 1 >= d /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
We thus obtain the following problem:
2:	T:
		(?, 1)    start(a, b, c, d, e, f, g, h) -> stop(a, h - 10, c, 1, e, h, g, h) [ a >= 101 /\ b = c /\ d = e /\ f = g /\ h = a ]
		(?, 1)    start(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, 2, e, h + 11, g, h) [ 100 >= a /\ b = c /\ d = e /\ f = g /\ h = a ]
		(?, 1)    lbl161(a, b, c, d, e, f, g, h) -> stop(a, b, c, d, e, f, g, h) [ 89 >= a /\ d = 1 /\ h = a /\ f = 101 /\ b = 91 ]
		(?, 1)    lbl221(a, b, c, d, e, f, g, h) -> lbl161(a, f - 20, c, d - 1, e, f - 10, g, h) [ 99 >= a /\ 89 >= a /\ f = 111 /\ d = 2 /\ h = a /\ b = c ]
		(?, 1)    lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ d >= 3 /\ 110 >= f /\ d >= 2 /\ f >= 102 /\ 111 >= f /\ f + 10 >= a + 11*d /\ 89 >= a /\ h = a /\ b = c ]
		(?, 1)    lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ d >= 2 /\ 110 >= f /\ f >= 102 /\ 111 >= f /\ f + 10 >= a + 11*d /\ 89 >= a /\ h = a /\ b = c ]
		(?, 1)    lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d - 1, e, f - 9, g, h) [ d >= 3 /\ d >= 2 /\ 121 >= a + 11*d /\ 89 >= a /\ f = 111 /\ h = a /\ b = c ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d + 1, e, f + 11, g, h) [ 111 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl161(a, f - 20, c, d - 1, e, f - 10, g, h) [ f = 111 /\ d = 2 /\ h = 100 /\ b = c /\ a = 100 ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ 11*d + a >= 112 /\ d >= 3 /\ 121 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ 11*d + a >= 112 /\ d >= 2 /\ 121 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d - 1, e, f - 9, g, h) [ d >= 3 /\ 11*d >= 22 /\ f = 111 /\ h + 11*d = 122 /\ b = c /\ a + 11*d = 122 ]
		(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, b, c, 2, e, h + 11, g, h) [ 100 >= a /\ b = c /\ d = e /\ f = g /\ h = a ]
		(?, 1)    lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ d >= 3 /\ 110 >= f /\ d >= 2 /\ f >= 102 /\ 111 >= f /\ f + 10 >= a + 11*d /\ 89 >= a /\ h = a /\ b = c ]
		(?, 1)    lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ d >= 2 /\ 110 >= f /\ f >= 102 /\ 111 >= f /\ f + 10 >= a + 11*d /\ 89 >= a /\ h = a /\ b = c ]
		(?, 1)    lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d - 1, e, f - 9, g, h) [ d >= 3 /\ d >= 2 /\ 121 >= a + 11*d /\ 89 >= a /\ f = 111 /\ h = a /\ b = c ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d + 1, e, f + 11, g, h) [ 111 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ 11*d + a >= 112 /\ d >= 3 /\ 121 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ 11*d + a >= 112 /\ d >= 2 /\ 121 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d - 1, e, f - 9, g, h) [ d >= 3 /\ 11*d >= 22 /\ f = 111 /\ h + 11*d = 122 /\ b = c /\ a + 11*d = 122 ]
		(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) -> lbl111(a, b, c, 2, e, h + 11, g, h) [ 100 >= a /\ b = c /\ d = e /\ f = g /\ h = a ]
		(?, 1)    lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ d >= 3 /\ 110 >= f /\ d >= 2 /\ f >= 102 /\ 111 >= f /\ f + 10 >= a + 11*d /\ 89 >= a /\ h = a /\ b = c ]
		(?, 1)    lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ d >= 2 /\ 110 >= f /\ f >= 102 /\ 111 >= f /\ f + 10 >= a + 11*d /\ 89 >= a /\ h = a /\ b = c ]
		(?, 1)    lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d - 1, e, f - 9, g, h) [ d >= 3 /\ d >= 2 /\ 121 >= a + 11*d /\ 89 >= a /\ f = 111 /\ h = a /\ b = c ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d + 1, e, f + 11, g, h) [ 111 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ 11*d + a >= 112 /\ d >= 3 /\ 121 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ 11*d + a >= 112 /\ d >= 2 /\ 121 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d - 1, e, f - 9, g, h) [ d >= 3 /\ 11*d >= 22 /\ f = 111 /\ h + 11*d = 122 /\ b = c /\ a + 11*d = 122 ]
		(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) = 1
	Pol(lbl111) = 1
	Pol(lbl221) = 0
	Pol(start0) = 1
orients all transitions weakly and the transitions
	lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ 11*d + a >= 112 /\ d >= 3 /\ 121 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
	lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ 11*d + a >= 112 /\ d >= 2 /\ 121 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
strictly and produces the following problem:
5:	T:
		(1, 1)    start(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, 2, e, h + 11, g, h) [ 100 >= a /\ b = c /\ d = e /\ f = g /\ h = a ]
		(?, 1)    lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ d >= 3 /\ 110 >= f /\ d >= 2 /\ f >= 102 /\ 111 >= f /\ f + 10 >= a + 11*d /\ 89 >= a /\ h = a /\ b = c ]
		(?, 1)    lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ d >= 2 /\ 110 >= f /\ f >= 102 /\ 111 >= f /\ f + 10 >= a + 11*d /\ 89 >= a /\ h = a /\ b = c ]
		(?, 1)    lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d - 1, e, f - 9, g, h) [ d >= 3 /\ d >= 2 /\ 121 >= a + 11*d /\ 89 >= a /\ f = 111 /\ h = a /\ b = c ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d + 1, e, f + 11, g, h) [ 111 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
		(1, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ 11*d + a >= 112 /\ d >= 3 /\ 121 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
		(1, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ 11*d + a >= 112 /\ d >= 2 /\ 121 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d - 1, e, f - 9, g, h) [ d >= 3 /\ 11*d >= 22 /\ f = 111 /\ h + 11*d = 122 /\ b = c /\ a + 11*d = 122 ]
		(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) = 1
	Pol(lbl111) = 1
	Pol(lbl221) = 0
	Pol(start0) = 1
orients all transitions weakly and the transition
	lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d - 1, e, f - 9, g, h) [ d >= 3 /\ 11*d >= 22 /\ f = 111 /\ h + 11*d = 122 /\ b = c /\ a + 11*d = 122 ]
strictly and produces the following problem:
6:	T:
		(1, 1)    start(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, 2, e, h + 11, g, h) [ 100 >= a /\ b = c /\ d = e /\ f = g /\ h = a ]
		(?, 1)    lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ d >= 3 /\ 110 >= f /\ d >= 2 /\ f >= 102 /\ 111 >= f /\ f + 10 >= a + 11*d /\ 89 >= a /\ h = a /\ b = c ]
		(?, 1)    lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ d >= 2 /\ 110 >= f /\ f >= 102 /\ 111 >= f /\ f + 10 >= a + 11*d /\ 89 >= a /\ h = a /\ b = c ]
		(?, 1)    lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d - 1, e, f - 9, g, h) [ d >= 3 /\ d >= 2 /\ 121 >= a + 11*d /\ 89 >= a /\ f = 111 /\ h = a /\ b = c ]
		(?, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d + 1, e, f + 11, g, h) [ 111 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
		(1, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ 11*d + a >= 112 /\ d >= 3 /\ 121 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
		(1, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ 11*d + a >= 112 /\ d >= 2 /\ 121 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
		(1, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d - 1, e, f - 9, g, h) [ d >= 3 /\ 11*d >= 22 /\ f = 111 /\ h + 11*d = 122 /\ b = c /\ a + 11*d = 122 ]
		(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) = -V_1 - V_8 + 201
	Pol(lbl111) = -V_1 - V_6 + 212
	Pol(lbl221) = 11*V_4 - V_6 + 92
	Pol(start0) = -2*V_1 + 201
orients all transitions weakly and the transitions
	lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ d >= 3 /\ 110 >= f /\ d >= 2 /\ f >= 102 /\ 111 >= f /\ f + 10 >= a + 11*d /\ 89 >= a /\ h = a /\ b = c ]
	lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ d >= 2 /\ 110 >= f /\ f >= 102 /\ 111 >= f /\ f + 10 >= a + 11*d /\ 89 >= a /\ h = a /\ b = c ]
	lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d - 1, e, f - 9, g, h) [ d >= 3 /\ d >= 2 /\ 121 >= a + 11*d /\ 89 >= a /\ f = 111 /\ h = a /\ b = c ]
	lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d + 1, e, f + 11, g, h) [ 111 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
strictly and produces the following problem:
7:	T:
		(1, 1)            start(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, 2, e, h + 11, g, h) [ 100 >= a /\ b = c /\ d = e /\ f = g /\ h = a ]
		(2*a + 201, 1)    lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ d >= 3 /\ 110 >= f /\ d >= 2 /\ f >= 102 /\ 111 >= f /\ f + 10 >= a + 11*d /\ 89 >= a /\ h = a /\ b = c ]
		(2*a + 201, 1)    lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ d >= 2 /\ 110 >= f /\ f >= 102 /\ 111 >= f /\ f + 10 >= a + 11*d /\ 89 >= a /\ h = a /\ b = c ]
		(2*a + 201, 1)    lbl221(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d - 1, e, f - 9, g, h) [ d >= 3 /\ d >= 2 /\ 121 >= a + 11*d /\ 89 >= a /\ f = 111 /\ h = a /\ b = c ]
		(2*a + 201, 1)    lbl111(a, b, c, d, e, f, g, h) -> lbl111(a, b, c, d + 1, e, f + 11, g, h) [ 111 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
		(1, 1)            lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ 11*d + a >= 112 /\ d >= 3 /\ 121 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
		(1, 1)            lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d, e, f + 1, g, h) [ 11*d + a >= 112 /\ d >= 2 /\ 121 >= 11*d + a /\ 122 >= 11*d + a /\ 11*d >= 22 /\ h = a /\ b = c /\ f + 11 = 11*d + a ]
		(1, 1)            lbl111(a, b, c, d, e, f, g, h) -> lbl221(a, b, c, d - 1, e, f - 9, g, h) [ d >= 3 /\ 11*d >= 22 /\ f = 111 /\ h + 11*d = 122 /\ b = c /\ a + 11*d = 122 ]
		(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 8*a + 813

Time: 0.890 sec (SMT: 0.829 sec)