YES(?, 72*a + 36*a^2 + 40)

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

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

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

A polynomial rank function with
	Pol(lbl91) = -2*V_5 + 2*V_7
	Pol(lbl131) = -2*V_5 + 2*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("lbl91(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, e + 1, f, g, h) [ e >= 0 /\\ g >= e + 1 /\\ a >= g /\\ d = a ]", 0-0) = a
	S("lbl91(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, e + 1, f, g, h) [ e >= 0 /\\ g >= e + 1 /\\ a >= g /\\ d = a ]", 0-1) = ?
	S("lbl91(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, e + 1, f, g, h) [ e >= 0 /\\ g >= e + 1 /\\ a >= g /\\ d = a ]", 0-2) = c
	S("lbl91(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, e + 1, f, g, h) [ e >= 0 /\\ g >= e + 1 /\\ a >= g /\\ d = a ]", 0-3) = a
	S("lbl91(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, e + 1, f, g, h) [ e >= 0 /\\ g >= e + 1 /\\ a >= g /\\ d = a ]", 0-4) = a
	S("lbl91(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, e + 1, f, g, h) [ e >= 0 /\\ g >= e + 1 /\\ a >= g /\\ d = a ]", 0-5) = f
	S("lbl91(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, e + 1, f, g, h) [ e >= 0 /\\ g >= e + 1 /\\ a >= g /\\ d = a ]", 0-6) = a
	S("lbl91(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, e + 1, f, g, h) [ e >= 0 /\\ g >= e + 1 /\\ a >= g /\\ d = a ]", 0-7) = h
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, e + 1, f, g, h) [ g >= e + 1 /\\ g >= e /\\ e >= 1 /\\ a >= g /\\ d = a ]", 0-0) = a
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, e + 1, f, g, h) [ g >= e + 1 /\\ g >= e /\\ e >= 1 /\\ a >= g /\\ d = a ]", 0-1) = ?
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, e + 1, f, g, h) [ g >= e + 1 /\\ g >= e /\\ e >= 1 /\\ a >= g /\\ d = a ]", 0-2) = c
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, e + 1, f, g, h) [ g >= e + 1 /\\ g >= e /\\ e >= 1 /\\ a >= g /\\ d = a ]", 0-3) = a
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, e + 1, f, g, h) [ g >= e + 1 /\\ g >= e /\\ e >= 1 /\\ a >= g /\\ d = a ]", 0-4) = a
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, e + 1, f, g, h) [ g >= e + 1 /\\ g >= e /\\ e >= 1 /\\ a >= g /\\ d = a ]", 0-5) = f
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, e + 1, f, g, h) [ g >= e + 1 /\\ g >= e /\\ e >= 1 /\\ a >= g /\\ d = a ]", 0-6) = a
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, e + 1, f, g, h) [ g >= e + 1 /\\ g >= e /\\ e >= 1 /\\ a >= g /\\ d = a ]", 0-7) = h
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, e, f, g, h) [ g >= e + 1 /\\ g >= e /\\ e >= 1 /\\ a >= g /\\ d = a ]", 0-0) = a
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, e, f, g, h) [ g >= e + 1 /\\ g >= e /\\ e >= 1 /\\ a >= g /\\ d = a ]", 0-1) = ?
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, e, f, g, h) [ g >= e + 1 /\\ g >= e /\\ e >= 1 /\\ a >= g /\\ d = a ]", 0-2) = c
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, e, f, g, h) [ g >= e + 1 /\\ g >= e /\\ e >= 1 /\\ a >= g /\\ d = a ]", 0-3) = a
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, e, f, g, h) [ g >= e + 1 /\\ g >= e /\\ e >= 1 /\\ a >= g /\\ d = a ]", 0-4) = a + 2
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, e, f, g, h) [ g >= e + 1 /\\ g >= e /\\ e >= 1 /\\ a >= g /\\ d = a ]", 0-5) = f
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, e, f, g, h) [ g >= e + 1 /\\ g >= e /\\ e >= 1 /\\ a >= g /\\ d = a ]", 0-6) = a
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, e, f, g, h) [ g >= e + 1 /\\ g >= e /\\ e >= 1 /\\ a >= g /\\ d = a ]", 0-7) = h
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl142(a, b, c, d, e, f, g - 1, h) [ g >= 1 /\\ a >= g /\\ e = g /\\ d = a ]", 0-0) = a
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl142(a, b, c, d, e, f, g - 1, h) [ g >= 1 /\\ a >= g /\\ e = g /\\ d = a ]", 0-1) = ?
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl142(a, b, c, d, e, f, g - 1, h) [ g >= 1 /\\ a >= g /\\ e = g /\\ d = a ]", 0-2) = c
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl142(a, b, c, d, e, f, g - 1, h) [ g >= 1 /\\ a >= g /\\ e = g /\\ d = a ]", 0-3) = a
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl142(a, b, c, d, e, f, g - 1, h) [ g >= 1 /\\ a >= g /\\ e = g /\\ d = a ]", 0-4) = a + 2
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl142(a, b, c, d, e, f, g - 1, h) [ g >= 1 /\\ a >= g /\\ e = g /\\ d = a ]", 0-5) = f
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl142(a, b, c, d, e, f, g - 1, h) [ g >= 1 /\\ a >= g /\\ e = g /\\ d = a ]", 0-6) = a
	S("lbl131(a, b, c, d, e, f, g, h) -> lbl142(a, b, c, d, e, f, g - 1, h) [ g >= 1 /\\ a >= g /\\ e = g /\\ d = a ]", 0-7) = h
	S("lbl142(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, 1, f, g, h) [ e >= 2 /\\ e >= 0 /\\ a >= e /\\ g + 1 = e /\\ d = a ]", 0-0) = a
	S("lbl142(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, 1, f, g, h) [ e >= 2 /\\ e >= 0 /\\ a >= e /\\ g + 1 = e /\\ d = a ]", 0-1) = ?
	S("lbl142(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, 1, f, g, h) [ e >= 2 /\\ e >= 0 /\\ a >= e /\\ g + 1 = e /\\ d = a ]", 0-2) = c
	S("lbl142(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, 1, f, g, h) [ e >= 2 /\\ e >= 0 /\\ a >= e /\\ g + 1 = e /\\ d = a ]", 0-3) = a
	S("lbl142(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, 1, f, g, h) [ e >= 2 /\\ e >= 0 /\\ a >= e /\\ g + 1 = e /\\ d = a ]", 0-4) = 1
	S("lbl142(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, 1, f, g, h) [ e >= 2 /\\ e >= 0 /\\ a >= e /\\ g + 1 = e /\\ d = a ]", 0-5) = f
	S("lbl142(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, 1, f, g, h) [ e >= 2 /\\ e >= 0 /\\ a >= e /\\ g + 1 = e /\\ d = a ]", 0-6) = a
	S("lbl142(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, 1, f, g, h) [ e >= 2 /\\ e >= 0 /\\ a >= e /\\ g + 1 = e /\\ d = a ]", 0-7) = h
	S("lbl142(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, 0, f, g, h) [ e >= 2 /\\ e >= 0 /\\ a >= e /\\ g + 1 = e /\\ d = a ]", 0-0) = a
	S("lbl142(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, 0, f, g, h) [ e >= 2 /\\ e >= 0 /\\ a >= e /\\ g + 1 = e /\\ d = a ]", 0-1) = ?
	S("lbl142(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, 0, f, g, h) [ e >= 2 /\\ e >= 0 /\\ a >= e /\\ g + 1 = e /\\ d = a ]", 0-2) = c
	S("lbl142(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, 0, f, g, h) [ e >= 2 /\\ e >= 0 /\\ a >= e /\\ g + 1 = e /\\ d = a ]", 0-3) = a
	S("lbl142(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, 0, f, g, h) [ e >= 2 /\\ e >= 0 /\\ a >= e /\\ g + 1 = e /\\ d = a ]", 0-4) = 0
	S("lbl142(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, 0, f, g, h) [ e >= 2 /\\ e >= 0 /\\ a >= e /\\ g + 1 = e /\\ d = a ]", 0-5) = f
	S("lbl142(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, 0, f, g, h) [ e >= 2 /\\ e >= 0 /\\ a >= e /\\ g + 1 = e /\\ d = a ]", 0-6) = a
	S("lbl142(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, 0, f, g, h) [ e >= 2 /\\ e >= 0 /\\ a >= e /\\ g + 1 = e /\\ d = a ]", 0-7) = h
	S("start(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, 1, f, d, h) [ a >= 1 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-0) = a
	S("start(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, 1, f, d, h) [ a >= 1 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-1) = c
	S("start(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, 1, f, d, h) [ a >= 1 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-2) = c
	S("start(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, 1, f, d, h) [ a >= 1 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-3) = a
	S("start(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, 1, f, d, h) [ a >= 1 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-4) = 1
	S("start(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, 1, f, d, h) [ a >= 1 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-5) = f
	S("start(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, 1, f, d, h) [ a >= 1 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-6) = a
	S("start(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, 1, f, d, h) [ a >= 1 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-7) = h
	S("start(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, 0, f, d, h) [ a >= 1 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-0) = a
	S("start(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, 0, f, d, h) [ a >= 1 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-1) = ?
	S("start(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, 0, f, d, h) [ a >= 1 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-2) = c
	S("start(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, 0, f, d, h) [ a >= 1 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-3) = a
	S("start(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, 0, f, d, h) [ a >= 1 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-4) = 0
	S("start(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, 0, f, d, h) [ a >= 1 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-5) = f
	S("start(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, 0, f, d, h) [ a >= 1 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-6) = a
	S("start(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, 0, f, d, h) [ a >= 1 /\\ b = c /\\ d = a /\\ e = f /\\ g = h ]", 0-7) = h
orients the transitions
	lbl91(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, e + 1, f, g, h) [ e >= 0 /\ g >= e + 1 /\ a >= g /\ d = a ]
	lbl131(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, e, f, g, h) [ g >= e + 1 /\ g >= e /\ e >= 1 /\ a >= g /\ d = a ]
	lbl131(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, e + 1, f, g, h) [ g >= e + 1 /\ g >= e /\ e >= 1 /\ a >= g /\ d = a ]
weakly and the transitions
	lbl91(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, e + 1, f, g, h) [ e >= 0 /\ g >= e + 1 /\ a >= g /\ d = a ]
	lbl131(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, e, f, g, h) [ g >= e + 1 /\ g >= e /\ e >= 1 /\ a >= g /\ d = a ]
	lbl131(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, e + 1, f, g, h) [ g >= e + 1 /\ g >= e /\ e >= 1 /\ a >= g /\ d = a ]
strictly and produces the following problem:
5:	T:
		(1, 1)                    start(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, 0, f, d, h) [ a >= 1 /\ b = c /\ d = a /\ e = f /\ g = h ]
		(1, 1)                    start(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, 1, f, d, h) [ a >= 1 /\ b = c /\ d = a /\ e = f /\ g = h ]
		(3*a + 2, 1)              lbl142(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, 0, f, g, h) [ e >= 2 /\ e >= 0 /\ a >= e /\ g + 1 = e /\ d = a ]
		(3*a + 2, 1)              lbl142(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, 1, f, g, h) [ e >= 2 /\ e >= 0 /\ a >= e /\ g + 1 = e /\ d = a ]
		(3*a + 2, 1)              lbl131(a, b, c, d, e, f, g, h) -> lbl142(a, b, c, d, e, f, g - 1, h) [ g >= 1 /\ a >= g /\ e = g /\ d = a ]
		(12*a^2 + 21*a + 9, 1)    lbl131(a, b, c, d, e, f, g, h) -> lbl91(a, i, c, d, e, f, g, h) [ g >= e + 1 /\ g >= e /\ e >= 1 /\ a >= g /\ d = a ]
		(12*a^2 + 21*a + 9, 1)    lbl131(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, e + 1, f, g, h) [ g >= e + 1 /\ g >= e /\ e >= 1 /\ a >= g /\ d = a ]
		(12*a^2 + 21*a + 9, 1)    lbl91(a, b, c, d, e, f, g, h) -> lbl131(a, b, c, d, e + 1, f, g, h) [ e >= 0 /\ g >= e + 1 /\ a >= g /\ 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:	4

Complexity upper bound 72*a + 36*a^2 + 40

Time: 0.526 sec (SMT: 0.484 sec)