YES(?, 3*a^2 + 22*a + 28)

Initial complexity problem:
1:	T:
		(?, 1)    start(a, b, c, d, e, f, g, h, i, j) -> stop(a, b, c, d, e, f, g, h, 1, j) [ 1 >= a /\ b = c /\ d = e /\ f = a /\ g = h /\ i = j ]
		(?, 1)    start(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, 1, j) [ a >= 2 /\ b = c /\ d = e /\ f = a /\ g = h /\ i = j ]
		(?, 1)    lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, g - 1, h, i, j) [ g >= 0 /\ i >= g + 2 /\ g + 1 >= 0 /\ a >= i + 1 /\ f = a ]
		(?, 1)    lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, g, h, i + 1, j) [ i >= g + 2 /\ g + 1 >= 0 /\ a >= i + 1 /\ f = a ]
		(?, 1)    lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, i - 2, h, i, j) [ i >= 1 /\ a >= i + 1 /\ f = a ]
		(?, 1)    lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, i - 1, h, i + 1, j) [ i >= 1 /\ a >= i + 1 /\ f = a ]
		(?, 1)    lbl13(a, b, c, d, e, f, g, h, i, j) -> stop(a, b, c, d, e, f, g, h, i, j) [ g + a >= 2 /\ g + 1 >= 0 /\ a >= g + 2 /\ f = a /\ i = a /\ d + 1 = a ]
		(?, 1)    lbl13(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, i, j) [ a >= d + 2 /\ g + d >= 1 /\ g + 1 >= 0 /\ a >= d + 1 /\ d >= g + 1 /\ f = a /\ i = d + 1 ]
		(1, 1)    start0(a, b, c, d, e, f, g, h, i, j) -> start(a, c, c, e, e, a, h, h, j, j)
	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, i, j) -> lbl31(a, k, c, d, e, f, g, h, 1, j) [ a >= 2 /\ b = c /\ d = e /\ f = a /\ g = h /\ i = j ]
		(?, 1)    lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, g - 1, h, i, j) [ g >= 0 /\ i >= g + 2 /\ g + 1 >= 0 /\ a >= i + 1 /\ f = a ]
		(?, 1)    lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, g, h, i + 1, j) [ i >= g + 2 /\ g + 1 >= 0 /\ a >= i + 1 /\ f = a ]
		(?, 1)    lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, i - 2, h, i, j) [ i >= 1 /\ a >= i + 1 /\ f = a ]
		(?, 1)    lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, i - 1, h, i + 1, j) [ i >= 1 /\ a >= i + 1 /\ f = a ]
		(?, 1)    lbl13(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, i, j) [ a >= d + 2 /\ g + d >= 1 /\ g + 1 >= 0 /\ a >= d + 1 /\ d >= g + 1 /\ f = a /\ i = d + 1 ]
		(1, 1)    start0(a, b, c, d, e, f, g, h, i, j) -> start(a, c, c, e, e, a, h, h, j, j)
	start location:	start0
	leaf cost:	2

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

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

A polynomial rank function with
	Pol(lbl43) = V_7 + 1
and size complexities
	S("start0(a, b, c, d, e, f, g, h, i, j) -> start(a, c, c, e, e, a, h, h, j, j)", 0-0) = a
	S("start0(a, b, c, d, e, f, g, h, i, j) -> start(a, c, c, e, e, a, h, h, j, j)", 0-1) = c
	S("start0(a, b, c, d, e, f, g, h, i, j) -> start(a, c, c, e, e, a, h, h, j, j)", 0-2) = c
	S("start0(a, b, c, d, e, f, g, h, i, j) -> start(a, c, c, e, e, a, h, h, j, j)", 0-3) = e
	S("start0(a, b, c, d, e, f, g, h, i, j) -> start(a, c, c, e, e, a, h, h, j, j)", 0-4) = e
	S("start0(a, b, c, d, e, f, g, h, i, j) -> start(a, c, c, e, e, a, h, h, j, j)", 0-5) = a
	S("start0(a, b, c, d, e, f, g, h, i, j) -> start(a, c, c, e, e, a, h, h, j, j)", 0-6) = h
	S("start0(a, b, c, d, e, f, g, h, i, j) -> start(a, c, c, e, e, a, h, h, j, j)", 0-7) = h
	S("start0(a, b, c, d, e, f, g, h, i, j) -> start(a, c, c, e, e, a, h, h, j, j)", 0-8) = j
	S("start0(a, b, c, d, e, f, g, h, i, j) -> start(a, c, c, e, e, a, h, h, j, j)", 0-9) = j
	S("lbl13(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, i, j) [ a >= d + 2 /\\ g + d >= 1 /\\ g + 1 >= 0 /\\ a >= d + 1 /\\ d >= g + 1 /\\ f = a /\\ i = d + 1 ]", 0-0) = a
	S("lbl13(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, i, j) [ a >= d + 2 /\\ g + d >= 1 /\\ g + 1 >= 0 /\\ a >= d + 1 /\\ d >= g + 1 /\\ f = a /\\ i = d + 1 ]", 0-1) = ?
	S("lbl13(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, i, j) [ a >= d + 2 /\\ g + d >= 1 /\\ g + 1 >= 0 /\\ a >= d + 1 /\\ d >= g + 1 /\\ f = a /\\ i = d + 1 ]", 0-2) = c
	S("lbl13(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, i, j) [ a >= d + 2 /\\ g + d >= 1 /\\ g + 1 >= 0 /\\ a >= d + 1 /\\ d >= g + 1 /\\ f = a /\\ i = d + 1 ]", 0-3) = a + 1
	S("lbl13(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, i, j) [ a >= d + 2 /\\ g + d >= 1 /\\ g + 1 >= 0 /\\ a >= d + 1 /\\ d >= g + 1 /\\ f = a /\\ i = d + 1 ]", 0-4) = e
	S("lbl13(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, i, j) [ a >= d + 2 /\\ g + d >= 1 /\\ g + 1 >= 0 /\\ a >= d + 1 /\\ d >= g + 1 /\\ f = a /\\ i = d + 1 ]", 0-5) = a
	S("lbl13(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, i, j) [ a >= d + 2 /\\ g + d >= 1 /\\ g + 1 >= 0 /\\ a >= d + 1 /\\ d >= g + 1 /\\ f = a /\\ i = d + 1 ]", 0-6) = a + 2
	S("lbl13(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, i, j) [ a >= d + 2 /\\ g + d >= 1 /\\ g + 1 >= 0 /\\ a >= d + 1 /\\ d >= g + 1 /\\ f = a /\\ i = d + 1 ]", 0-7) = h
	S("lbl13(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, i, j) [ a >= d + 2 /\\ g + d >= 1 /\\ g + 1 >= 0 /\\ a >= d + 1 /\\ d >= g + 1 /\\ f = a /\\ i = d + 1 ]", 0-8) = a
	S("lbl13(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, i, j) [ a >= d + 2 /\\ g + d >= 1 /\\ g + 1 >= 0 /\\ a >= d + 1 /\\ d >= g + 1 /\\ f = a /\\ i = d + 1 ]", 0-9) = j
	S("lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, i - 1, h, i + 1, j) [ i >= 1 /\\ a >= i + 1 /\\ f = a ]", 0-0) = a
	S("lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, i - 1, h, i + 1, j) [ i >= 1 /\\ a >= i + 1 /\\ f = a ]", 0-1) = ?
	S("lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, i - 1, h, i + 1, j) [ i >= 1 /\\ a >= i + 1 /\\ f = a ]", 0-2) = c
	S("lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, i - 1, h, i + 1, j) [ i >= 1 /\\ a >= i + 1 /\\ f = a ]", 0-3) = a + 1
	S("lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, i - 1, h, i + 1, j) [ i >= 1 /\\ a >= i + 1 /\\ f = a ]", 0-4) = e
	S("lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, i - 1, h, i + 1, j) [ i >= 1 /\\ a >= i + 1 /\\ f = a ]", 0-5) = a
	S("lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, i - 1, h, i + 1, j) [ i >= 1 /\\ a >= i + 1 /\\ f = a ]", 0-6) = a + 1
	S("lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, i - 1, h, i + 1, j) [ i >= 1 /\\ a >= i + 1 /\\ f = a ]", 0-7) = h
	S("lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, i - 1, h, i + 1, j) [ i >= 1 /\\ a >= i + 1 /\\ f = a ]", 0-8) = a
	S("lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, i - 1, h, i + 1, j) [ i >= 1 /\\ a >= i + 1 /\\ f = a ]", 0-9) = j
	S("lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, i - 2, h, i, j) [ i >= 1 /\\ a >= i + 1 /\\ f = a ]", 0-0) = a
	S("lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, i - 2, h, i, j) [ i >= 1 /\\ a >= i + 1 /\\ f = a ]", 0-1) = ?
	S("lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, i - 2, h, i, j) [ i >= 1 /\\ a >= i + 1 /\\ f = a ]", 0-2) = c
	S("lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, i - 2, h, i, j) [ i >= 1 /\\ a >= i + 1 /\\ f = a ]", 0-3) = a + e + 1
	S("lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, i - 2, h, i, j) [ i >= 1 /\\ a >= i + 1 /\\ f = a ]", 0-4) = e
	S("lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, i - 2, h, i, j) [ i >= 1 /\\ a >= i + 1 /\\ f = a ]", 0-5) = a
	S("lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, i - 2, h, i, j) [ i >= 1 /\\ a >= i + 1 /\\ f = a ]", 0-6) = a + 1
	S("lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, i - 2, h, i, j) [ i >= 1 /\\ a >= i + 1 /\\ f = a ]", 0-7) = h
	S("lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, i - 2, h, i, j) [ i >= 1 /\\ a >= i + 1 /\\ f = a ]", 0-8) = a + 1
	S("lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, i - 2, h, i, j) [ i >= 1 /\\ a >= i + 1 /\\ f = a ]", 0-9) = j
	S("lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, g, h, i + 1, j) [ i >= g + 2 /\\ g + 1 >= 0 /\\ a >= i + 1 /\\ f = a ]", 0-0) = a
	S("lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, g, h, i + 1, j) [ i >= g + 2 /\\ g + 1 >= 0 /\\ a >= i + 1 /\\ f = a ]", 0-1) = ?
	S("lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, g, h, i + 1, j) [ i >= g + 2 /\\ g + 1 >= 0 /\\ a >= i + 1 /\\ f = a ]", 0-2) = c
	S("lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, g, h, i + 1, j) [ i >= g + 2 /\\ g + 1 >= 0 /\\ a >= i + 1 /\\ f = a ]", 0-3) = a + 1
	S("lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, g, h, i + 1, j) [ i >= g + 2 /\\ g + 1 >= 0 /\\ a >= i + 1 /\\ f = a ]", 0-4) = e
	S("lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, g, h, i + 1, j) [ i >= g + 2 /\\ g + 1 >= 0 /\\ a >= i + 1 /\\ f = a ]", 0-5) = a
	S("lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, g, h, i + 1, j) [ i >= g + 2 /\\ g + 1 >= 0 /\\ a >= i + 1 /\\ f = a ]", 0-6) = a + 2
	S("lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, g, h, i + 1, j) [ i >= g + 2 /\\ g + 1 >= 0 /\\ a >= i + 1 /\\ f = a ]", 0-7) = h
	S("lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, g, h, i + 1, j) [ i >= g + 2 /\\ g + 1 >= 0 /\\ a >= i + 1 /\\ f = a ]", 0-8) = a
	S("lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, g, h, i + 1, j) [ i >= g + 2 /\\ g + 1 >= 0 /\\ a >= i + 1 /\\ f = a ]", 0-9) = j
	S("lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, g - 1, h, i, j) [ g >= 0 /\\ i >= g + 2 /\\ g + 1 >= 0 /\\ a >= i + 1 /\\ f = a ]", 0-0) = a
	S("lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, g - 1, h, i, j) [ g >= 0 /\\ i >= g + 2 /\\ g + 1 >= 0 /\\ a >= i + 1 /\\ f = a ]", 0-1) = ?
	S("lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, g - 1, h, i, j) [ g >= 0 /\\ i >= g + 2 /\\ g + 1 >= 0 /\\ a >= i + 1 /\\ f = a ]", 0-2) = c
	S("lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, g - 1, h, i, j) [ g >= 0 /\\ i >= g + 2 /\\ g + 1 >= 0 /\\ a >= i + 1 /\\ f = a ]", 0-3) = a + e + 1
	S("lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, g - 1, h, i, j) [ g >= 0 /\\ i >= g + 2 /\\ g + 1 >= 0 /\\ a >= i + 1 /\\ f = a ]", 0-4) = e
	S("lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, g - 1, h, i, j) [ g >= 0 /\\ i >= g + 2 /\\ g + 1 >= 0 /\\ a >= i + 1 /\\ f = a ]", 0-5) = a
	S("lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, g - 1, h, i, j) [ g >= 0 /\\ i >= g + 2 /\\ g + 1 >= 0 /\\ a >= i + 1 /\\ f = a ]", 0-6) = a + 2
	S("lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, g - 1, h, i, j) [ g >= 0 /\\ i >= g + 2 /\\ g + 1 >= 0 /\\ a >= i + 1 /\\ f = a ]", 0-7) = h
	S("lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, g - 1, h, i, j) [ g >= 0 /\\ i >= g + 2 /\\ g + 1 >= 0 /\\ a >= i + 1 /\\ f = a ]", 0-8) = a + 1
	S("lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, g - 1, h, i, j) [ g >= 0 /\\ i >= g + 2 /\\ g + 1 >= 0 /\\ a >= i + 1 /\\ f = a ]", 0-9) = j
	S("start(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, 1, j) [ a >= 2 /\\ b = c /\\ d = e /\\ f = a /\\ g = h /\\ i = j ]", 0-0) = a
	S("start(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, 1, j) [ a >= 2 /\\ b = c /\\ d = e /\\ f = a /\\ g = h /\\ i = j ]", 0-1) = ?
	S("start(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, 1, j) [ a >= 2 /\\ b = c /\\ d = e /\\ f = a /\\ g = h /\\ i = j ]", 0-2) = c
	S("start(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, 1, j) [ a >= 2 /\\ b = c /\\ d = e /\\ f = a /\\ g = h /\\ i = j ]", 0-3) = e
	S("start(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, 1, j) [ a >= 2 /\\ b = c /\\ d = e /\\ f = a /\\ g = h /\\ i = j ]", 0-4) = e
	S("start(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, 1, j) [ a >= 2 /\\ b = c /\\ d = e /\\ f = a /\\ g = h /\\ i = j ]", 0-5) = a
	S("start(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, 1, j) [ a >= 2 /\\ b = c /\\ d = e /\\ f = a /\\ g = h /\\ i = j ]", 0-6) = h
	S("start(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, 1, j) [ a >= 2 /\\ b = c /\\ d = e /\\ f = a /\\ g = h /\\ i = j ]", 0-7) = h
	S("start(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, 1, j) [ a >= 2 /\\ b = c /\\ d = e /\\ f = a /\\ g = h /\\ i = j ]", 0-8) = 1
	S("start(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, 1, j) [ a >= 2 /\\ b = c /\\ d = e /\\ f = a /\\ g = h /\\ i = j ]", 0-9) = j
orients the transition
	lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, g - 1, h, i, j) [ g >= 0 /\ i >= g + 2 /\ g + 1 >= 0 /\ a >= i + 1 /\ f = a ]
weakly and the transition
	lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, g - 1, h, i, j) [ g >= 0 /\ i >= g + 2 /\ g + 1 >= 0 /\ a >= i + 1 /\ f = a ]
strictly and produces the following problem:
5:	T:
		(1, 1)                   start(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, 1, j) [ a >= 2 /\ b = c /\ d = e /\ f = a /\ g = h /\ i = j ]
		(3*a^2 + 10*a + 8, 1)    lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, g - 1, h, i, j) [ g >= 0 /\ i >= g + 2 /\ g + 1 >= 0 /\ a >= i + 1 /\ f = a ]
		(3*a + 4, 1)             lbl43(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, g, h, i + 1, j) [ i >= g + 2 /\ g + 1 >= 0 /\ a >= i + 1 /\ f = a ]
		(3*a + 4, 1)             lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl43(a, b, c, d, e, f, i - 2, h, i, j) [ i >= 1 /\ a >= i + 1 /\ f = a ]
		(3*a + 4, 1)             lbl31(a, b, c, d, e, f, g, h, i, j) -> lbl13(a, b, c, i, e, f, i - 1, h, i + 1, j) [ i >= 1 /\ a >= i + 1 /\ f = a ]
		(3*a + 4, 1)             lbl13(a, b, c, d, e, f, g, h, i, j) -> lbl31(a, k, c, d, e, f, g, h, i, j) [ a >= d + 2 /\ g + d >= 1 /\ g + 1 >= 0 /\ a >= d + 1 /\ d >= g + 1 /\ f = a /\ i = d + 1 ]
		(1, 1)                   start0(a, b, c, d, e, f, g, h, i, j) -> start(a, c, c, e, e, a, h, h, j, j)
	start location:	start0
	leaf cost:	2

Complexity upper bound 3*a^2 + 22*a + 28

Time: 0.536 sec (SMT: 0.497 sec)