YES(?, 2318416846246180*a + 2318416846246176*b + 4*e + 55800*a^2 + 110700*a*b + 54900*b^2 + 54900*a*e + 54900*b*e + 4)

Initial complexity problem:
1:	T:
		(?, 1)    f2(a, b, c, d, e, f, g, h) -> f8(a, b, 0, b, e, f, g, h) [ a >= b + 1 ]
		(?, 1)    f8(a, b, c, d, e, f, g, h) -> f8(a, b, c, d, e + 1, j, i, h) [ a >= e /\ i >= j ]
		(?, 1)    f8(a, b, c, d, e, f, g, h) -> f8(a, b, j, e, e + 1, i, k, h) [ a >= e /\ i >= k + 1 ]
		(?, 1)    f19(a, b, c, d, e, f, g, h) -> f19(a, b, c, d, e + 1, f, g, j) [ a >= e ]
		(?, 1)    f27(a, b, c, d, e, f, g, h) -> f27(a, b, c, d, e + 1, f, g, j) [ a >= e ]
		(?, 1)    f34(a, b, c, d, e, f, g, h) -> f36(a, b, c, d, e, f, g, h) [ 0 >= c + 1 ]
		(?, 1)    f34(a, b, c, d, e, f, g, h) -> f36(a, b, c, d, e, f, g, h) [ c >= 1 ]
		(?, 1)    f36(a, b, c, d, e, f, g, h) -> f43(a, b, c, d, e, f, g, j) [ 0 >= i + 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
		(?, 1)    f36(a, b, c, d, e, f, g, h) -> f43(a, b, c, d, e, f, g, j) [ i >= 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
		(?, 1)    f43(a, b, c, d, e, f, g, h) -> f43(a, b, c, d, e + 1, f, g, h) [ a >= e ]
		(?, 1)    f49(a, b, c, d, e, f, g, h) -> f49(a, b, c, d, e + 1, f, g, h) [ a >= e ]
		(?, 1)    f36(a, b, c, d, e, f, g, h) -> f36(a, b, c, d + 1, e, f, g, 0) [ a >= d ]
		(?, 1)    f34(a, b, c, d, e, f, g, h) -> f2(a, b + 1, 0, d, e, f, g, h) [ c = 0 ]
		(?, 1)    f49(a, b, c, d, e, f, g, h) -> f36(a, b, c, d + 1, e, f, g, h) [ e >= a + 1 ]
		(?, 1)    f43(a, b, c, d, e, f, g, h) -> f49(a, b, c, d, e, f, g, h) [ e >= a + 1 ]
		(?, 1)    f36(a, b, c, d, e, f, g, h) -> f2(a, b + 1, c, d, e, f, g, h) [ d >= a + 1 ]
		(?, 1)    f27(a, b, c, d, e, f, g, h) -> f34(a, b, c, d, e, f, g, h) [ e >= a + 1 ]
		(?, 1)    f19(a, b, c, d, e, f, g, h) -> f27(a, b, c, d, e, f, g, h) [ e >= a + 1 ]
		(?, 1)    f8(a, b, c, d, e, f, g, h) -> f34(a, b, c, b, e, f, g, h) [ e >= a + 1 /\ b = d ]
		(?, 1)    f8(a, b, c, d, e, f, g, h) -> f19(a, b, c, d, e, f, g, h) [ b >= d + 1 /\ e >= a + 1 ]
		(?, 1)    f8(a, b, c, d, e, f, g, h) -> f19(a, b, c, d, e, f, g, h) [ d >= b + 1 /\ e >= a + 1 ]
		(?, 1)    f2(a, b, c, d, e, f, g, h) -> f1(a, b, c, d, e, f, g, h) [ b >= a ]
		(1, 1)    start(a, b, c, d, e, f, g, h) -> f2(a, b, c, d, e, f, g, h)
	start location:	start
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c, d, e].
We thus obtain the following problem:
2:	T:
		(1, 1)    start(a, b, c, d, e) -> f2(a, b, c, d, e)
		(?, 1)    f2(a, b, c, d, e) -> f1(a, b, c, d, e) [ b >= a ]
		(?, 1)    f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ d >= b + 1 /\ e >= a + 1 ]
		(?, 1)    f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ b >= d + 1 /\ e >= a + 1 ]
		(?, 1)    f8(a, b, c, d, e) -> f34(a, b, c, b, e) [ e >= a + 1 /\ b = d ]
		(?, 1)    f19(a, b, c, d, e) -> f27(a, b, c, d, e) [ e >= a + 1 ]
		(?, 1)    f27(a, b, c, d, e) -> f34(a, b, c, d, e) [ e >= a + 1 ]
		(?, 1)    f36(a, b, c, d, e) -> f2(a, b + 1, c, d, e) [ d >= a + 1 ]
		(?, 1)    f43(a, b, c, d, e) -> f49(a, b, c, d, e) [ e >= a + 1 ]
		(?, 1)    f49(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ e >= a + 1 ]
		(?, 1)    f34(a, b, c, d, e) -> f2(a, b + 1, 0, d, e) [ c = 0 ]
		(?, 1)    f36(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ a >= d ]
		(?, 1)    f49(a, b, c, d, e) -> f49(a, b, c, d, e + 1) [ a >= e ]
		(?, 1)    f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]
		(?, 1)    f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ i >= 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
		(?, 1)    f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ 0 >= i + 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
		(?, 1)    f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ c >= 1 ]
		(?, 1)    f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ 0 >= c + 1 ]
		(?, 1)    f27(a, b, c, d, e) -> f27(a, b, c, d, e + 1) [ a >= e ]
		(?, 1)    f19(a, b, c, d, e) -> f19(a, b, c, d, e + 1) [ a >= e ]
		(?, 1)    f8(a, b, c, d, e) -> f8(a, b, j, e, e + 1) [ a >= e /\ i >= k + 1 ]
		(?, 1)    f8(a, b, c, d, e) -> f8(a, b, c, d, e + 1) [ a >= e /\ i >= j ]
		(?, 1)    f2(a, b, c, d, e) -> f8(a, b, 0, b, e) [ a >= b + 1 ]
	start location:	start
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem:
3:	T:
		(1, 1)    start(a, b, c, d, e) -> f2(a, b, c, d, e)
		(?, 1)    f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ d >= b + 1 /\ e >= a + 1 ]
		(?, 1)    f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ b >= d + 1 /\ e >= a + 1 ]
		(?, 1)    f8(a, b, c, d, e) -> f34(a, b, c, b, e) [ e >= a + 1 /\ b = d ]
		(?, 1)    f19(a, b, c, d, e) -> f27(a, b, c, d, e) [ e >= a + 1 ]
		(?, 1)    f27(a, b, c, d, e) -> f34(a, b, c, d, e) [ e >= a + 1 ]
		(?, 1)    f36(a, b, c, d, e) -> f2(a, b + 1, c, d, e) [ d >= a + 1 ]
		(?, 1)    f43(a, b, c, d, e) -> f49(a, b, c, d, e) [ e >= a + 1 ]
		(?, 1)    f49(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ e >= a + 1 ]
		(?, 1)    f34(a, b, c, d, e) -> f2(a, b + 1, 0, d, e) [ c = 0 ]
		(?, 1)    f36(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ a >= d ]
		(?, 1)    f49(a, b, c, d, e) -> f49(a, b, c, d, e + 1) [ a >= e ]
		(?, 1)    f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]
		(?, 1)    f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ i >= 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
		(?, 1)    f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ 0 >= i + 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
		(?, 1)    f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ c >= 1 ]
		(?, 1)    f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ 0 >= c + 1 ]
		(?, 1)    f27(a, b, c, d, e) -> f27(a, b, c, d, e + 1) [ a >= e ]
		(?, 1)    f19(a, b, c, d, e) -> f19(a, b, c, d, e + 1) [ a >= e ]
		(?, 1)    f8(a, b, c, d, e) -> f8(a, b, j, e, e + 1) [ a >= e /\ i >= k + 1 ]
		(?, 1)    f8(a, b, c, d, e) -> f8(a, b, c, d, e + 1) [ a >= e /\ i >= j ]
		(?, 1)    f2(a, b, c, d, e) -> f8(a, b, 0, b, e) [ a >= b + 1 ]
	start location:	start
	leaf cost:	1

Testing for reachability in the complexity graph removes the following transitions from problem 3:
	f49(a, b, c, d, e) -> f49(a, b, c, d, e + 1) [ a >= e ]
	f27(a, b, c, d, e) -> f27(a, b, c, d, e + 1) [ a >= e ]
	f19(a, b, c, d, e) -> f19(a, b, c, d, e + 1) [ a >= e ]
We thus obtain the following problem:
4:	T:
		(?, 1)    f49(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ e >= a + 1 ]
		(?, 1)    f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]
		(?, 1)    f43(a, b, c, d, e) -> f49(a, b, c, d, e) [ e >= a + 1 ]
		(?, 1)    f27(a, b, c, d, e) -> f34(a, b, c, d, e) [ e >= a + 1 ]
		(?, 1)    f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ 0 >= i + 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
		(?, 1)    f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ i >= 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
		(?, 1)    f36(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ a >= d ]
		(?, 1)    f36(a, b, c, d, e) -> f2(a, b + 1, c, d, e) [ d >= a + 1 ]
		(?, 1)    f19(a, b, c, d, e) -> f27(a, b, c, d, e) [ e >= a + 1 ]
		(?, 1)    f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ b >= d + 1 /\ e >= a + 1 ]
		(?, 1)    f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ d >= b + 1 /\ e >= a + 1 ]
		(?, 1)    f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ 0 >= c + 1 ]
		(?, 1)    f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ c >= 1 ]
		(?, 1)    f34(a, b, c, d, e) -> f2(a, b + 1, 0, d, e) [ c = 0 ]
		(?, 1)    f8(a, b, c, d, e) -> f8(a, b, c, d, e + 1) [ a >= e /\ i >= j ]
		(?, 1)    f8(a, b, c, d, e) -> f8(a, b, j, e, e + 1) [ a >= e /\ i >= k + 1 ]
		(?, 1)    f8(a, b, c, d, e) -> f34(a, b, c, b, e) [ e >= a + 1 /\ b = d ]
		(?, 1)    f2(a, b, c, d, e) -> f8(a, b, 0, b, e) [ a >= b + 1 ]
		(1, 1)    start(a, b, c, d, e) -> f2(a, b, c, d, e)
	start location:	start
	leaf cost:	1

A polynomial rank function with
	Pol(f49) = 6*V_1 - 6*V_2 - 5
	Pol(f36) = 6*V_1 - 6*V_2 - 5
	Pol(f43) = 6*V_1 - 6*V_2 - 5
	Pol(f27) = 6*V_1 - 6*V_2 - 3
	Pol(f34) = 6*V_1 - 6*V_2 - 4
	Pol(f2) = 6*V_1 - 6*V_2
	Pol(f19) = 6*V_1 - 6*V_2 - 2
	Pol(f8) = 6*V_1 - 6*V_2 - 1
	Pol(start) = 6*V_1 - 6*V_2
orients all transitions weakly and the transition
	f2(a, b, c, d, e) -> f8(a, b, 0, b, e) [ a >= b + 1 ]
strictly and produces the following problem:
5:	T:
		(?, 1)            f49(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ e >= a + 1 ]
		(?, 1)            f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]
		(?, 1)            f43(a, b, c, d, e) -> f49(a, b, c, d, e) [ e >= a + 1 ]
		(?, 1)            f27(a, b, c, d, e) -> f34(a, b, c, d, e) [ e >= a + 1 ]
		(?, 1)            f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ 0 >= i + 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
		(?, 1)            f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ i >= 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
		(?, 1)            f36(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ a >= d ]
		(?, 1)            f36(a, b, c, d, e) -> f2(a, b + 1, c, d, e) [ d >= a + 1 ]
		(?, 1)            f19(a, b, c, d, e) -> f27(a, b, c, d, e) [ e >= a + 1 ]
		(?, 1)            f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ b >= d + 1 /\ e >= a + 1 ]
		(?, 1)            f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ d >= b + 1 /\ e >= a + 1 ]
		(?, 1)            f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ 0 >= c + 1 ]
		(?, 1)            f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ c >= 1 ]
		(?, 1)            f34(a, b, c, d, e) -> f2(a, b + 1, 0, d, e) [ c = 0 ]
		(?, 1)            f8(a, b, c, d, e) -> f8(a, b, c, d, e + 1) [ a >= e /\ i >= j ]
		(?, 1)            f8(a, b, c, d, e) -> f8(a, b, j, e, e + 1) [ a >= e /\ i >= k + 1 ]
		(?, 1)            f8(a, b, c, d, e) -> f34(a, b, c, b, e) [ e >= a + 1 /\ b = d ]
		(6*a + 6*b, 1)    f2(a, b, c, d, e) -> f8(a, b, 0, b, e) [ a >= b + 1 ]
		(1, 1)            start(a, b, c, d, e) -> f2(a, b, c, d, e)
	start location:	start
	leaf cost:	1

A polynomial rank function with
	Pol(f8) = 5
	Pol(f34) = 2
	Pol(f19) = 4
	Pol(f49) = 1
	Pol(f36) = 1
	Pol(f43) = 1
	Pol(f2) = 0
	Pol(f27) = 3
and size complexities
	S("start(a, b, c, d, e) -> f2(a, b, c, d, e)", 0-0) = a
	S("start(a, b, c, d, e) -> f2(a, b, c, d, e)", 0-1) = b
	S("start(a, b, c, d, e) -> f2(a, b, c, d, e)", 0-2) = c
	S("start(a, b, c, d, e) -> f2(a, b, c, d, e)", 0-3) = d
	S("start(a, b, c, d, e) -> f2(a, b, c, d, e)", 0-4) = e
	S("f2(a, b, c, d, e) -> f8(a, b, 0, b, e) [ a >= b + 1 ]", 0-0) = a
	S("f2(a, b, c, d, e) -> f8(a, b, 0, b, e) [ a >= b + 1 ]", 0-1) = ?
	S("f2(a, b, c, d, e) -> f8(a, b, 0, b, e) [ a >= b + 1 ]", 0-2) = 0
	S("f2(a, b, c, d, e) -> f8(a, b, 0, b, e) [ a >= b + 1 ]", 0-3) = ?
	S("f2(a, b, c, d, e) -> f8(a, b, 0, b, e) [ a >= b + 1 ]", 0-4) = ?
	S("f8(a, b, c, d, e) -> f34(a, b, c, b, e) [ e >= a + 1 /\\ b = d ]", 0-0) = a
	S("f8(a, b, c, d, e) -> f34(a, b, c, b, e) [ e >= a + 1 /\\ b = d ]", 0-1) = ?
	S("f8(a, b, c, d, e) -> f34(a, b, c, b, e) [ e >= a + 1 /\\ b = d ]", 0-2) = ?
	S("f8(a, b, c, d, e) -> f34(a, b, c, b, e) [ e >= a + 1 /\\ b = d ]", 0-3) = ?
	S("f8(a, b, c, d, e) -> f34(a, b, c, b, e) [ e >= a + 1 /\\ b = d ]", 0-4) = ?
	S("f8(a, b, c, d, e) -> f8(a, b, j, e, e + 1) [ a >= e /\\ i >= k + 1 ]", 0-0) = a
	S("f8(a, b, c, d, e) -> f8(a, b, j, e, e + 1) [ a >= e /\\ i >= k + 1 ]", 0-1) = ?
	S("f8(a, b, c, d, e) -> f8(a, b, j, e, e + 1) [ a >= e /\\ i >= k + 1 ]", 0-2) = ?
	S("f8(a, b, c, d, e) -> f8(a, b, j, e, e + 1) [ a >= e /\\ i >= k + 1 ]", 0-3) = ?
	S("f8(a, b, c, d, e) -> f8(a, b, j, e, e + 1) [ a >= e /\\ i >= k + 1 ]", 0-4) = ?
	S("f8(a, b, c, d, e) -> f8(a, b, c, d, e + 1) [ a >= e /\\ i >= j ]", 0-0) = a
	S("f8(a, b, c, d, e) -> f8(a, b, c, d, e + 1) [ a >= e /\\ i >= j ]", 0-1) = ?
	S("f8(a, b, c, d, e) -> f8(a, b, c, d, e + 1) [ a >= e /\\ i >= j ]", 0-2) = ?
	S("f8(a, b, c, d, e) -> f8(a, b, c, d, e + 1) [ a >= e /\\ i >= j ]", 0-3) = ?
	S("f8(a, b, c, d, e) -> f8(a, b, c, d, e + 1) [ a >= e /\\ i >= j ]", 0-4) = ?
	S("f34(a, b, c, d, e) -> f2(a, b + 1, 0, d, e) [ c = 0 ]", 0-0) = a
	S("f34(a, b, c, d, e) -> f2(a, b + 1, 0, d, e) [ c = 0 ]", 0-1) = ?
	S("f34(a, b, c, d, e) -> f2(a, b + 1, 0, d, e) [ c = 0 ]", 0-2) = 0
	S("f34(a, b, c, d, e) -> f2(a, b + 1, 0, d, e) [ c = 0 ]", 0-3) = ?
	S("f34(a, b, c, d, e) -> f2(a, b + 1, 0, d, e) [ c = 0 ]", 0-4) = ?
	S("f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ c >= 1 ]", 0-0) = a
	S("f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ c >= 1 ]", 0-1) = ?
	S("f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ c >= 1 ]", 0-2) = ?
	S("f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ c >= 1 ]", 0-3) = ?
	S("f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ c >= 1 ]", 0-4) = ?
	S("f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ 0 >= c + 1 ]", 0-0) = a
	S("f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ 0 >= c + 1 ]", 0-1) = ?
	S("f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ 0 >= c + 1 ]", 0-2) = ?
	S("f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ 0 >= c + 1 ]", 0-3) = ?
	S("f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ 0 >= c + 1 ]", 0-4) = ?
	S("f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ d >= b + 1 /\\ e >= a + 1 ]", 0-0) = a
	S("f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ d >= b + 1 /\\ e >= a + 1 ]", 0-1) = ?
	S("f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ d >= b + 1 /\\ e >= a + 1 ]", 0-2) = ?
	S("f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ d >= b + 1 /\\ e >= a + 1 ]", 0-3) = ?
	S("f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ d >= b + 1 /\\ e >= a + 1 ]", 0-4) = ?
	S("f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ b >= d + 1 /\\ e >= a + 1 ]", 0-0) = a
	S("f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ b >= d + 1 /\\ e >= a + 1 ]", 0-1) = ?
	S("f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ b >= d + 1 /\\ e >= a + 1 ]", 0-2) = ?
	S("f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ b >= d + 1 /\\ e >= a + 1 ]", 0-3) = ?
	S("f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ b >= d + 1 /\\ e >= a + 1 ]", 0-4) = ?
	S("f19(a, b, c, d, e) -> f27(a, b, c, d, e) [ e >= a + 1 ]", 0-0) = a
	S("f19(a, b, c, d, e) -> f27(a, b, c, d, e) [ e >= a + 1 ]", 0-1) = ?
	S("f19(a, b, c, d, e) -> f27(a, b, c, d, e) [ e >= a + 1 ]", 0-2) = ?
	S("f19(a, b, c, d, e) -> f27(a, b, c, d, e) [ e >= a + 1 ]", 0-3) = ?
	S("f19(a, b, c, d, e) -> f27(a, b, c, d, e) [ e >= a + 1 ]", 0-4) = ?
	S("f36(a, b, c, d, e) -> f2(a, b + 1, c, d, e) [ d >= a + 1 ]", 0-0) = a
	S("f36(a, b, c, d, e) -> f2(a, b + 1, c, d, e) [ d >= a + 1 ]", 0-1) = ?
	S("f36(a, b, c, d, e) -> f2(a, b + 1, c, d, e) [ d >= a + 1 ]", 0-2) = ?
	S("f36(a, b, c, d, e) -> f2(a, b + 1, c, d, e) [ d >= a + 1 ]", 0-3) = ?
	S("f36(a, b, c, d, e) -> f2(a, b + 1, c, d, e) [ d >= a + 1 ]", 0-4) = ?
	S("f36(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ a >= d ]", 0-0) = a
	S("f36(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ a >= d ]", 0-1) = ?
	S("f36(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ a >= d ]", 0-2) = ?
	S("f36(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ a >= d ]", 0-3) = ?
	S("f36(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ a >= d ]", 0-4) = ?
	S("f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ i >= 1 /\\ a >= d /\\ i >= c*k /\\ c*k + k >= i + 1 /\\ k >= j /\\ i >= c*l /\\ c*l + l >= i + 1 /\\ j >= l ]", 0-0) = a
	S("f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ i >= 1 /\\ a >= d /\\ i >= c*k /\\ c*k + k >= i + 1 /\\ k >= j /\\ i >= c*l /\\ c*l + l >= i + 1 /\\ j >= l ]", 0-1) = ?
	S("f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ i >= 1 /\\ a >= d /\\ i >= c*k /\\ c*k + k >= i + 1 /\\ k >= j /\\ i >= c*l /\\ c*l + l >= i + 1 /\\ j >= l ]", 0-2) = ?
	S("f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ i >= 1 /\\ a >= d /\\ i >= c*k /\\ c*k + k >= i + 1 /\\ k >= j /\\ i >= c*l /\\ c*l + l >= i + 1 /\\ j >= l ]", 0-3) = ?
	S("f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ i >= 1 /\\ a >= d /\\ i >= c*k /\\ c*k + k >= i + 1 /\\ k >= j /\\ i >= c*l /\\ c*l + l >= i + 1 /\\ j >= l ]", 0-4) = ?
	S("f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ 0 >= i + 1 /\\ a >= d /\\ i >= c*k /\\ c*k + k >= i + 1 /\\ k >= j /\\ i >= c*l /\\ c*l + l >= i + 1 /\\ j >= l ]", 0-0) = a
	S("f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ 0 >= i + 1 /\\ a >= d /\\ i >= c*k /\\ c*k + k >= i + 1 /\\ k >= j /\\ i >= c*l /\\ c*l + l >= i + 1 /\\ j >= l ]", 0-1) = ?
	S("f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ 0 >= i + 1 /\\ a >= d /\\ i >= c*k /\\ c*k + k >= i + 1 /\\ k >= j /\\ i >= c*l /\\ c*l + l >= i + 1 /\\ j >= l ]", 0-2) = ?
	S("f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ 0 >= i + 1 /\\ a >= d /\\ i >= c*k /\\ c*k + k >= i + 1 /\\ k >= j /\\ i >= c*l /\\ c*l + l >= i + 1 /\\ j >= l ]", 0-3) = ?
	S("f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ 0 >= i + 1 /\\ a >= d /\\ i >= c*k /\\ c*k + k >= i + 1 /\\ k >= j /\\ i >= c*l /\\ c*l + l >= i + 1 /\\ j >= l ]", 0-4) = ?
	S("f27(a, b, c, d, e) -> f34(a, b, c, d, e) [ e >= a + 1 ]", 0-0) = a
	S("f27(a, b, c, d, e) -> f34(a, b, c, d, e) [ e >= a + 1 ]", 0-1) = ?
	S("f27(a, b, c, d, e) -> f34(a, b, c, d, e) [ e >= a + 1 ]", 0-2) = ?
	S("f27(a, b, c, d, e) -> f34(a, b, c, d, e) [ e >= a + 1 ]", 0-3) = ?
	S("f27(a, b, c, d, e) -> f34(a, b, c, d, e) [ e >= a + 1 ]", 0-4) = ?
	S("f43(a, b, c, d, e) -> f49(a, b, c, d, e) [ e >= a + 1 ]", 0-0) = a
	S("f43(a, b, c, d, e) -> f49(a, b, c, d, e) [ e >= a + 1 ]", 0-1) = ?
	S("f43(a, b, c, d, e) -> f49(a, b, c, d, e) [ e >= a + 1 ]", 0-2) = ?
	S("f43(a, b, c, d, e) -> f49(a, b, c, d, e) [ e >= a + 1 ]", 0-3) = ?
	S("f43(a, b, c, d, e) -> f49(a, b, c, d, e) [ e >= a + 1 ]", 0-4) = ?
	S("f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]", 0-0) = a
	S("f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]", 0-1) = ?
	S("f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]", 0-2) = ?
	S("f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]", 0-3) = ?
	S("f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]", 0-4) = ?
	S("f49(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ e >= a + 1 ]", 0-0) = a
	S("f49(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ e >= a + 1 ]", 0-1) = ?
	S("f49(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ e >= a + 1 ]", 0-2) = ?
	S("f49(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ e >= a + 1 ]", 0-3) = ?
	S("f49(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ e >= a + 1 ]", 0-4) = ?
orients the transitions
	f8(a, b, c, d, e) -> f8(a, b, j, e, e + 1) [ a >= e /\ i >= k + 1 ]
	f8(a, b, c, d, e) -> f8(a, b, c, d, e + 1) [ a >= e /\ i >= j ]
	f8(a, b, c, d, e) -> f34(a, b, c, b, e) [ e >= a + 1 /\ b = d ]
	f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ d >= b + 1 /\ e >= a + 1 ]
	f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ b >= d + 1 /\ e >= a + 1 ]
	f49(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ e >= a + 1 ]
	f43(a, b, c, d, e) -> f49(a, b, c, d, e) [ e >= a + 1 ]
	f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]
	f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ i >= 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
	f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ 0 >= i + 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
	f36(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ a >= d ]
	f36(a, b, c, d, e) -> f2(a, b + 1, c, d, e) [ d >= a + 1 ]
	f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ c >= 1 ]
	f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ 0 >= c + 1 ]
	f34(a, b, c, d, e) -> f2(a, b + 1, 0, d, e) [ c = 0 ]
	f27(a, b, c, d, e) -> f34(a, b, c, d, e) [ e >= a + 1 ]
	f19(a, b, c, d, e) -> f27(a, b, c, d, e) [ e >= a + 1 ]
weakly and the transitions
	f8(a, b, c, d, e) -> f34(a, b, c, b, e) [ e >= a + 1 /\ b = d ]
	f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ d >= b + 1 /\ e >= a + 1 ]
	f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ b >= d + 1 /\ e >= a + 1 ]
	f36(a, b, c, d, e) -> f2(a, b + 1, c, d, e) [ d >= a + 1 ]
	f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ c >= 1 ]
	f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ 0 >= c + 1 ]
	f34(a, b, c, d, e) -> f2(a, b + 1, 0, d, e) [ c = 0 ]
	f27(a, b, c, d, e) -> f34(a, b, c, d, e) [ e >= a + 1 ]
	f19(a, b, c, d, e) -> f27(a, b, c, d, e) [ e >= a + 1 ]
strictly and produces the following problem:
6:	T:
		(?, 1)              f49(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ e >= a + 1 ]
		(?, 1)              f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]
		(?, 1)              f43(a, b, c, d, e) -> f49(a, b, c, d, e) [ e >= a + 1 ]
		(30*a + 30*b, 1)    f27(a, b, c, d, e) -> f34(a, b, c, d, e) [ e >= a + 1 ]
		(?, 1)              f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ 0 >= i + 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
		(?, 1)              f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ i >= 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
		(?, 1)              f36(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ a >= d ]
		(30*a + 30*b, 1)    f36(a, b, c, d, e) -> f2(a, b + 1, c, d, e) [ d >= a + 1 ]
		(30*a + 30*b, 1)    f19(a, b, c, d, e) -> f27(a, b, c, d, e) [ e >= a + 1 ]
		(30*a + 30*b, 1)    f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ b >= d + 1 /\ e >= a + 1 ]
		(30*a + 30*b, 1)    f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ d >= b + 1 /\ e >= a + 1 ]
		(30*a + 30*b, 1)    f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ 0 >= c + 1 ]
		(30*a + 30*b, 1)    f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ c >= 1 ]
		(30*a + 30*b, 1)    f34(a, b, c, d, e) -> f2(a, b + 1, 0, d, e) [ c = 0 ]
		(?, 1)              f8(a, b, c, d, e) -> f8(a, b, c, d, e + 1) [ a >= e /\ i >= j ]
		(?, 1)              f8(a, b, c, d, e) -> f8(a, b, j, e, e + 1) [ a >= e /\ i >= k + 1 ]
		(30*a + 30*b, 1)    f8(a, b, c, d, e) -> f34(a, b, c, b, e) [ e >= a + 1 /\ b = d ]
		(6*a + 6*b, 1)      f2(a, b, c, d, e) -> f8(a, b, 0, b, e) [ a >= b + 1 ]
		(1, 1)              start(a, b, c, d, e) -> f2(a, b, c, d, e)
	start location:	start
	leaf cost:	1

A polynomial rank function with
	Pol(f49) = 2*V_1 - 2*V_5 + 1
	Pol(f36) = 2*V_1 - 2*V_5 + 1
	Pol(f43) = 2*V_1 - 2*V_5 + 1
	Pol(f27) = 2*V_1 - 2*V_5 + 1
	Pol(f34) = 2*V_1 - 2*V_5 + 1
	Pol(f2) = 2*V_1 - 2*V_5 + 1
	Pol(f19) = 2*V_1 - 2*V_5 + 1
	Pol(f8) = 2*V_1 - 2*V_5 + 1
	Pol(start) = 2*V_1 - 2*V_5 + 1
orients all transitions weakly and the transitions
	f8(a, b, c, d, e) -> f8(a, b, j, e, e + 1) [ a >= e /\ i >= k + 1 ]
	f8(a, b, c, d, e) -> f8(a, b, c, d, e + 1) [ a >= e /\ i >= j ]
	f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]
strictly and produces the following problem:
7:	T:
		(?, 1)                f49(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ e >= a + 1 ]
		(2*a + 2*e + 1, 1)    f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]
		(?, 1)                f43(a, b, c, d, e) -> f49(a, b, c, d, e) [ e >= a + 1 ]
		(30*a + 30*b, 1)      f27(a, b, c, d, e) -> f34(a, b, c, d, e) [ e >= a + 1 ]
		(?, 1)                f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ 0 >= i + 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
		(?, 1)                f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ i >= 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
		(?, 1)                f36(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ a >= d ]
		(30*a + 30*b, 1)      f36(a, b, c, d, e) -> f2(a, b + 1, c, d, e) [ d >= a + 1 ]
		(30*a + 30*b, 1)      f19(a, b, c, d, e) -> f27(a, b, c, d, e) [ e >= a + 1 ]
		(30*a + 30*b, 1)      f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ b >= d + 1 /\ e >= a + 1 ]
		(30*a + 30*b, 1)      f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ d >= b + 1 /\ e >= a + 1 ]
		(30*a + 30*b, 1)      f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ 0 >= c + 1 ]
		(30*a + 30*b, 1)      f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ c >= 1 ]
		(30*a + 30*b, 1)      f34(a, b, c, d, e) -> f2(a, b + 1, 0, d, e) [ c = 0 ]
		(2*a + 2*e + 1, 1)    f8(a, b, c, d, e) -> f8(a, b, c, d, e + 1) [ a >= e /\ i >= j ]
		(2*a + 2*e + 1, 1)    f8(a, b, c, d, e) -> f8(a, b, j, e, e + 1) [ a >= e /\ i >= k + 1 ]
		(30*a + 30*b, 1)      f8(a, b, c, d, e) -> f34(a, b, c, b, e) [ e >= a + 1 /\ b = d ]
		(6*a + 6*b, 1)        f2(a, b, c, d, e) -> f8(a, b, 0, b, e) [ a >= b + 1 ]
		(1, 1)                start(a, b, c, d, e) -> f2(a, b, c, d, e)
	start location:	start
	leaf cost:	1

Applied AI with 'oct' on problem 7 to obtain the following invariants:
  For symbol f19: -X_2 + X_5 - 2 >= 0 /\ -X_1 + X_5 - 1 >= 0 /\ X_1 - X_2 - 1 >= 0
  For symbol f27: -X_2 + X_5 - 2 >= 0 /\ -X_1 + X_5 - 1 >= 0 /\ X_1 - X_2 - 1 >= 0
  For symbol f34: -X_2 + X_5 - 2 >= 0 /\ -X_1 + X_5 - 1 >= 0 /\ X_1 - X_2 - 1 >= 0
  For symbol f36: -X_2 + X_5 - 2 >= 0 /\ -X_1 + X_5 - 1 >= 0 /\ X_1 - X_2 - 1 >= 0
  For symbol f43: -X_4 + X_5 - 1 >= 0 /\ -X_2 + X_5 - 2 >= 0 /\ -X_1 + X_5 - 1 >= 0 /\ X_1 - X_4 >= 0 /\ X_1 - X_2 - 1 >= 0
  For symbol f49: -X_4 + X_5 - 1 >= 0 /\ -X_2 + X_5 - 2 >= 0 /\ -X_1 + X_5 - 1 >= 0 /\ X_1 - X_4 >= 0 /\ X_1 - X_2 - 1 >= 0
  For symbol f8: X_1 - X_2 - 1 >= 0


This yielded the following problem:
8:	T:
		(1, 1)                start(a, b, c, d, e) -> f2(a, b, c, d, e)
		(6*a + 6*b, 1)        f2(a, b, c, d, e) -> f8(a, b, 0, b, e) [ a >= b + 1 ]
		(30*a + 30*b, 1)      f8(a, b, c, d, e) -> f34(a, b, c, b, e) [ a - b - 1 >= 0 /\ e >= a + 1 /\ b = d ]
		(2*a + 2*e + 1, 1)    f8(a, b, c, d, e) -> f8(a, b, j, e, e + 1) [ a - b - 1 >= 0 /\ a >= e /\ i >= k + 1 ]
		(2*a + 2*e + 1, 1)    f8(a, b, c, d, e) -> f8(a, b, c, d, e + 1) [ a - b - 1 >= 0 /\ a >= e /\ i >= j ]
		(30*a + 30*b, 1)      f34(a, b, c, d, e) -> f2(a, b + 1, 0, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ c = 0 ]
		(30*a + 30*b, 1)      f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ c >= 1 ]
		(30*a + 30*b, 1)      f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ 0 >= c + 1 ]
		(30*a + 30*b, 1)      f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ a - b - 1 >= 0 /\ d >= b + 1 /\ e >= a + 1 ]
		(30*a + 30*b, 1)      f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ a - b - 1 >= 0 /\ b >= d + 1 /\ e >= a + 1 ]
		(30*a + 30*b, 1)      f19(a, b, c, d, e) -> f27(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ]
		(30*a + 30*b, 1)      f36(a, b, c, d, e) -> f2(a, b + 1, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ d >= a + 1 ]
		(?, 1)                f36(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ a >= d ]
		(?, 1)                f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ i >= 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
		(?, 1)                f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ 0 >= i + 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
		(30*a + 30*b, 1)      f27(a, b, c, d, e) -> f34(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ]
		(?, 1)                f43(a, b, c, d, e) -> f49(a, b, c, d, e) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ]
		(2*a + 2*e + 1, 1)    f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ a >= e ]
		(?, 1)                f49(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ]
	start location:	start
	leaf cost:	1

Testing for unsatisfiable constraints removes the following transition from problem 8:
	f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ a >= e ]
We thus obtain the following problem:
9:	T:
		(1, 1)                start(a, b, c, d, e) -> f2(a, b, c, d, e)
		(6*a + 6*b, 1)        f2(a, b, c, d, e) -> f8(a, b, 0, b, e) [ a >= b + 1 ]
		(30*a + 30*b, 1)      f8(a, b, c, d, e) -> f34(a, b, c, b, e) [ a - b - 1 >= 0 /\ e >= a + 1 /\ b = d ]
		(2*a + 2*e + 1, 1)    f8(a, b, c, d, e) -> f8(a, b, j, e, e + 1) [ a - b - 1 >= 0 /\ a >= e /\ i >= k + 1 ]
		(2*a + 2*e + 1, 1)    f8(a, b, c, d, e) -> f8(a, b, c, d, e + 1) [ a - b - 1 >= 0 /\ a >= e /\ i >= j ]
		(30*a + 30*b, 1)      f34(a, b, c, d, e) -> f2(a, b + 1, 0, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ c = 0 ]
		(30*a + 30*b, 1)      f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ c >= 1 ]
		(30*a + 30*b, 1)      f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ 0 >= c + 1 ]
		(30*a + 30*b, 1)      f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ a - b - 1 >= 0 /\ d >= b + 1 /\ e >= a + 1 ]
		(30*a + 30*b, 1)      f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ a - b - 1 >= 0 /\ b >= d + 1 /\ e >= a + 1 ]
		(30*a + 30*b, 1)      f19(a, b, c, d, e) -> f27(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ]
		(30*a + 30*b, 1)      f36(a, b, c, d, e) -> f2(a, b + 1, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ d >= a + 1 ]
		(?, 1)                f36(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ a >= d ]
		(?, 1)                f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ i >= 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
		(?, 1)                f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ 0 >= i + 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
		(30*a + 30*b, 1)      f27(a, b, c, d, e) -> f34(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ]
		(?, 1)                f43(a, b, c, d, e) -> f49(a, b, c, d, e) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ]
		(?, 1)                f49(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ]
	start location:	start
	leaf cost:	1

A polynomial rank function with
	Pol(f49) = 3*V_1 - 3*V_4 + 1
	Pol(f36) = 3*V_1 - 3*V_4 + 3
	Pol(f43) = 3*V_1 - 3*V_4 + 2
and size complexities
	S("f49(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ -d + e - 1 >= 0 /\\ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - d >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-0) = a
	S("f49(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ -d + e - 1 >= 0 /\\ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - d >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-1) = 61*a + 61*b
	S("f49(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ -d + e - 1 >= 0 /\\ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - d >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-2) = ?
	S("f49(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ -d + e - 1 >= 0 /\\ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - d >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-3) = ?
	S("f49(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ -d + e - 1 >= 0 /\\ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - d >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-4) = 5*a + 5*e + 50
	S("f43(a, b, c, d, e) -> f49(a, b, c, d, e) [ -d + e - 1 >= 0 /\\ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - d >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-0) = a
	S("f43(a, b, c, d, e) -> f49(a, b, c, d, e) [ -d + e - 1 >= 0 /\\ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - d >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-1) = 61*a + 61*b
	S("f43(a, b, c, d, e) -> f49(a, b, c, d, e) [ -d + e - 1 >= 0 /\\ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - d >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-2) = ?
	S("f43(a, b, c, d, e) -> f49(a, b, c, d, e) [ -d + e - 1 >= 0 /\\ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - d >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-3) = ?
	S("f43(a, b, c, d, e) -> f49(a, b, c, d, e) [ -d + e - 1 >= 0 /\\ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - d >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-4) = 5*a + 5*e + 50
	S("f27(a, b, c, d, e) -> f34(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-0) = a
	S("f27(a, b, c, d, e) -> f34(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-1) = 61*a + 61*b
	S("f27(a, b, c, d, e) -> f34(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-2) = ?
	S("f27(a, b, c, d, e) -> f34(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-3) = 61*a + 61*b + 61*e + 42229815050
	S("f27(a, b, c, d, e) -> f34(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-4) = 5*a + 5*e + 50
	S("f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ 0 >= i + 1 /\\ a >= d /\\ i >= c*k /\\ c*k + k >= i + 1 /\\ k >= j /\\ i >= c*l /\\ c*l + l >= i + 1 /\\ j >= l ]", 0-0) = a
	S("f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ 0 >= i + 1 /\\ a >= d /\\ i >= c*k /\\ c*k + k >= i + 1 /\\ k >= j /\\ i >= c*l /\\ c*l + l >= i + 1 /\\ j >= l ]", 0-1) = 61*a + 61*b
	S("f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ 0 >= i + 1 /\\ a >= d /\\ i >= c*k /\\ c*k + k >= i + 1 /\\ k >= j /\\ i >= c*l /\\ c*l + l >= i + 1 /\\ j >= l ]", 0-2) = ?
	S("f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ 0 >= i + 1 /\\ a >= d /\\ i >= c*k /\\ c*k + k >= i + 1 /\\ k >= j /\\ i >= c*l /\\ c*l + l >= i + 1 /\\ j >= l ]", 0-3) = ?
	S("f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ 0 >= i + 1 /\\ a >= d /\\ i >= c*k /\\ c*k + k >= i + 1 /\\ k >= j /\\ i >= c*l /\\ c*l + l >= i + 1 /\\ j >= l ]", 0-4) = 5*a + 5*e + 50
	S("f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ i >= 1 /\\ a >= d /\\ i >= c*k /\\ c*k + k >= i + 1 /\\ k >= j /\\ i >= c*l /\\ c*l + l >= i + 1 /\\ j >= l ]", 0-0) = a
	S("f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ i >= 1 /\\ a >= d /\\ i >= c*k /\\ c*k + k >= i + 1 /\\ k >= j /\\ i >= c*l /\\ c*l + l >= i + 1 /\\ j >= l ]", 0-1) = 61*a + 61*b
	S("f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ i >= 1 /\\ a >= d /\\ i >= c*k /\\ c*k + k >= i + 1 /\\ k >= j /\\ i >= c*l /\\ c*l + l >= i + 1 /\\ j >= l ]", 0-2) = ?
	S("f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ i >= 1 /\\ a >= d /\\ i >= c*k /\\ c*k + k >= i + 1 /\\ k >= j /\\ i >= c*l /\\ c*l + l >= i + 1 /\\ j >= l ]", 0-3) = ?
	S("f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ i >= 1 /\\ a >= d /\\ i >= c*k /\\ c*k + k >= i + 1 /\\ k >= j /\\ i >= c*l /\\ c*l + l >= i + 1 /\\ j >= l ]", 0-4) = 5*a + 5*e + 50
	S("f36(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ a >= d ]", 0-0) = a
	S("f36(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ a >= d ]", 0-1) = 61*a + 61*b
	S("f36(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ a >= d ]", 0-2) = ?
	S("f36(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ a >= d ]", 0-3) = ?
	S("f36(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ a >= d ]", 0-4) = 5*a + 5*e + 50
	S("f36(a, b, c, d, e) -> f2(a, b + 1, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ d >= a + 1 ]", 0-0) = a
	S("f36(a, b, c, d, e) -> f2(a, b + 1, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ d >= a + 1 ]", 0-1) = 61*a + 61*b
	S("f36(a, b, c, d, e) -> f2(a, b + 1, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ d >= a + 1 ]", 0-2) = ?
	S("f36(a, b, c, d, e) -> f2(a, b + 1, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ d >= a + 1 ]", 0-3) = ?
	S("f36(a, b, c, d, e) -> f2(a, b + 1, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ d >= a + 1 ]", 0-4) = 5*a + 5*e + 50
	S("f19(a, b, c, d, e) -> f27(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-0) = a
	S("f19(a, b, c, d, e) -> f27(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-1) = 61*a + 61*b
	S("f19(a, b, c, d, e) -> f27(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-2) = ?
	S("f19(a, b, c, d, e) -> f27(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-3) = 61*a + 61*b + 61*e + 692292050
	S("f19(a, b, c, d, e) -> f27(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-4) = 5*a + 5*e + 50
	S("f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ a - b - 1 >= 0 /\\ b >= d + 1 /\\ e >= a + 1 ]", 0-0) = a
	S("f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ a - b - 1 >= 0 /\\ b >= d + 1 /\\ e >= a + 1 ]", 0-1) = 61*a + 61*b
	S("f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ a - b - 1 >= 0 /\\ b >= d + 1 /\\ e >= a + 1 ]", 0-2) = ?
	S("f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ a - b - 1 >= 0 /\\ b >= d + 1 /\\ e >= a + 1 ]", 0-3) = 61*a + 61*b + 61*e + 11349050
	S("f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ a - b - 1 >= 0 /\\ b >= d + 1 /\\ e >= a + 1 ]", 0-4) = 5*a + 5*e + 50
	S("f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ a - b - 1 >= 0 /\\ d >= b + 1 /\\ e >= a + 1 ]", 0-0) = a
	S("f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ a - b - 1 >= 0 /\\ d >= b + 1 /\\ e >= a + 1 ]", 0-1) = 61*a + 61*b
	S("f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ a - b - 1 >= 0 /\\ d >= b + 1 /\\ e >= a + 1 ]", 0-2) = ?
	S("f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ a - b - 1 >= 0 /\\ d >= b + 1 /\\ e >= a + 1 ]", 0-3) = 61*a + 61*b + 61*e + 11349050
	S("f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ a - b - 1 >= 0 /\\ d >= b + 1 /\\ e >= a + 1 ]", 0-4) = 5*a + 5*e + 50
	S("f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ 0 >= c + 1 ]", 0-0) = a
	S("f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ 0 >= c + 1 ]", 0-1) = 61*a + 61*b
	S("f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ 0 >= c + 1 ]", 0-2) = ?
	S("f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ 0 >= c + 1 ]", 0-3) = 61*a + 61*b + 61*e + 2576018718050
	S("f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ 0 >= c + 1 ]", 0-4) = 5*a + 5*e + 50
	S("f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ c >= 1 ]", 0-0) = a
	S("f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ c >= 1 ]", 0-1) = 61*a + 61*b
	S("f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ c >= 1 ]", 0-2) = ?
	S("f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ c >= 1 ]", 0-3) = 61*a + 61*b + 61*e + 2576018718050
	S("f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ c >= 1 ]", 0-4) = 5*a + 5*e + 50
	S("f34(a, b, c, d, e) -> f2(a, b + 1, 0, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ c = 0 ]", 0-0) = a
	S("f34(a, b, c, d, e) -> f2(a, b + 1, 0, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ c = 0 ]", 0-1) = 61*a + 61*b
	S("f34(a, b, c, d, e) -> f2(a, b + 1, 0, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ c = 0 ]", 0-2) = 0
	S("f34(a, b, c, d, e) -> f2(a, b + 1, 0, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ c = 0 ]", 0-3) = 61*a + 61*b + 61*e + 2576018718050
	S("f34(a, b, c, d, e) -> f2(a, b + 1, 0, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ c = 0 ]", 0-4) = 5*a + 5*e + 50
	S("f8(a, b, c, d, e) -> f8(a, b, c, d, e + 1) [ a - b - 1 >= 0 /\\ a >= e /\\ i >= j ]", 0-0) = a
	S("f8(a, b, c, d, e) -> f8(a, b, c, d, e + 1) [ a - b - 1 >= 0 /\\ a >= e /\\ i >= j ]", 0-1) = 61*a + 61*b
	S("f8(a, b, c, d, e) -> f8(a, b, c, d, e + 1) [ a - b - 1 >= 0 /\\ a >= e /\\ i >= j ]", 0-2) = ?
	S("f8(a, b, c, d, e) -> f8(a, b, c, d, e + 1) [ a - b - 1 >= 0 /\\ a >= e /\\ i >= j ]", 0-3) = 61*a + 61*b + 61*e + 186050
	S("f8(a, b, c, d, e) -> f8(a, b, c, d, e + 1) [ a - b - 1 >= 0 /\\ a >= e /\\ i >= j ]", 0-4) = 5*a + 5*e + 50
	S("f8(a, b, c, d, e) -> f8(a, b, j, e, e + 1) [ a - b - 1 >= 0 /\\ a >= e /\\ i >= k + 1 ]", 0-0) = a
	S("f8(a, b, c, d, e) -> f8(a, b, j, e, e + 1) [ a - b - 1 >= 0 /\\ a >= e /\\ i >= k + 1 ]", 0-1) = 61*a + 61*b
	S("f8(a, b, c, d, e) -> f8(a, b, j, e, e + 1) [ a - b - 1 >= 0 /\\ a >= e /\\ i >= k + 1 ]", 0-2) = ?
	S("f8(a, b, c, d, e) -> f8(a, b, j, e, e + 1) [ a - b - 1 >= 0 /\\ a >= e /\\ i >= k + 1 ]", 0-3) = 5*a + 5*e + 250
	S("f8(a, b, c, d, e) -> f8(a, b, j, e, e + 1) [ a - b - 1 >= 0 /\\ a >= e /\\ i >= k + 1 ]", 0-4) = 5*a + 5*e + 50
	S("f8(a, b, c, d, e) -> f34(a, b, c, b, e) [ a - b - 1 >= 0 /\\ e >= a + 1 /\\ b = d ]", 0-0) = a
	S("f8(a, b, c, d, e) -> f34(a, b, c, b, e) [ a - b - 1 >= 0 /\\ e >= a + 1 /\\ b = d ]", 0-1) = 61*a + 61*b
	S("f8(a, b, c, d, e) -> f34(a, b, c, b, e) [ a - b - 1 >= 0 /\\ e >= a + 1 /\\ b = d ]", 0-2) = ?
	S("f8(a, b, c, d, e) -> f34(a, b, c, b, e) [ a - b - 1 >= 0 /\\ e >= a + 1 /\\ b = d ]", 0-3) = 61*a + 61*b
	S("f8(a, b, c, d, e) -> f34(a, b, c, b, e) [ a - b - 1 >= 0 /\\ e >= a + 1 /\\ b = d ]", 0-4) = 5*a + 5*e + 50
	S("f2(a, b, c, d, e) -> f8(a, b, 0, b, e) [ a >= b + 1 ]", 0-0) = a
	S("f2(a, b, c, d, e) -> f8(a, b, 0, b, e) [ a >= b + 1 ]", 0-1) = 61*a + 61*b
	S("f2(a, b, c, d, e) -> f8(a, b, 0, b, e) [ a >= b + 1 ]", 0-2) = 0
	S("f2(a, b, c, d, e) -> f8(a, b, 0, b, e) [ a >= b + 1 ]", 0-3) = 61*a + 61*b
	S("f2(a, b, c, d, e) -> f8(a, b, 0, b, e) [ a >= b + 1 ]", 0-4) = 5*a + 5*e + 50
	S("start(a, b, c, d, e) -> f2(a, b, c, d, e)", 0-0) = a
	S("start(a, b, c, d, e) -> f2(a, b, c, d, e)", 0-1) = b
	S("start(a, b, c, d, e) -> f2(a, b, c, d, e)", 0-2) = c
	S("start(a, b, c, d, e) -> f2(a, b, c, d, e)", 0-3) = d
	S("start(a, b, c, d, e) -> f2(a, b, c, d, e)", 0-4) = e
orients the transitions
	f49(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ]
	f43(a, b, c, d, e) -> f49(a, b, c, d, e) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ]
	f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ i >= 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
	f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ 0 >= i + 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
	f36(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ a >= d ]
weakly and the transitions
	f49(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ]
	f43(a, b, c, d, e) -> f49(a, b, c, d, e) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ]
	f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ i >= 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
	f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ 0 >= i + 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
	f36(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ a >= d ]
strictly and produces the following problem:
10:	T:
		(1, 1)                                                                                                    start(a, b, c, d, e) -> f2(a, b, c, d, e)
		(6*a + 6*b, 1)                                                                                            f2(a, b, c, d, e) -> f8(a, b, 0, b, e) [ a >= b + 1 ]
		(30*a + 30*b, 1)                                                                                          f8(a, b, c, d, e) -> f34(a, b, c, b, e) [ a - b - 1 >= 0 /\ e >= a + 1 /\ b = d ]
		(2*a + 2*e + 1, 1)                                                                                        f8(a, b, c, d, e) -> f8(a, b, j, e, e + 1) [ a - b - 1 >= 0 /\ a >= e /\ i >= k + 1 ]
		(2*a + 2*e + 1, 1)                                                                                        f8(a, b, c, d, e) -> f8(a, b, c, d, e + 1) [ a - b - 1 >= 0 /\ a >= e /\ i >= j ]
		(30*a + 30*b, 1)                                                                                          f34(a, b, c, d, e) -> f2(a, b + 1, 0, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ c = 0 ]
		(30*a + 30*b, 1)                                                                                          f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ c >= 1 ]
		(30*a + 30*b, 1)                                                                                          f34(a, b, c, d, e) -> f36(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ 0 >= c + 1 ]
		(30*a + 30*b, 1)                                                                                          f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ a - b - 1 >= 0 /\ d >= b + 1 /\ e >= a + 1 ]
		(30*a + 30*b, 1)                                                                                          f8(a, b, c, d, e) -> f19(a, b, c, d, e) [ a - b - 1 >= 0 /\ b >= d + 1 /\ e >= a + 1 ]
		(30*a + 30*b, 1)                                                                                          f19(a, b, c, d, e) -> f27(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ]
		(30*a + 30*b, 1)                                                                                          f36(a, b, c, d, e) -> f2(a, b + 1, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ d >= a + 1 ]
		(11160*a^2 + 22140*a*b + 10980*b^2 + 10980*a*e + 10980*b*e + 463683369249180*a + 463683369249180*b, 1)    f36(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ a >= d ]
		(11160*a^2 + 22140*a*b + 10980*b^2 + 10980*a*e + 10980*b*e + 463683369249180*a + 463683369249180*b, 1)    f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ i >= 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
		(11160*a^2 + 22140*a*b + 10980*b^2 + 10980*a*e + 10980*b*e + 463683369249180*a + 463683369249180*b, 1)    f36(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ 0 >= i + 1 /\ a >= d /\ i >= c*k /\ c*k + k >= i + 1 /\ k >= j /\ i >= c*l /\ c*l + l >= i + 1 /\ j >= l ]
		(30*a + 30*b, 1)                                                                                          f27(a, b, c, d, e) -> f34(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ]
		(11160*a^2 + 22140*a*b + 10980*b^2 + 10980*a*e + 10980*b*e + 463683369249180*a + 463683369249180*b, 1)    f43(a, b, c, d, e) -> f49(a, b, c, d, e) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ]
		(11160*a^2 + 22140*a*b + 10980*b^2 + 10980*a*e + 10980*b*e + 463683369249180*a + 463683369249180*b, 1)    f49(a, b, c, d, e) -> f36(a, b, c, d + 1, e) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ]
	start location:	start
	leaf cost:	1

Complexity upper bound 2318416846246180*a + 2318416846246176*b + 4*e + 55800*a^2 + 110700*a*b + 54900*b^2 + 54900*a*e + 54900*b*e + 4

Time: 1.495 sec (SMT: 1.351 sec)