YES(?, a + b + 4)

Initial complexity problem:
1:	T:
		(?, 1)    f2(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f2(a, b + 1, b1*c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) [ a >= b ]
		(?, 1)    f10(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f19(a, b, c, d, b1, q1, d1, g1, l1, 1, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) [ d >= 2*c1 /\ 3*c1 >= d + 1 /\ c1 >= d1 /\ d >= 2*e1 /\ 3*e1 >= d + 1 /\ d1 >= e1 /\ b1*d >= 2*b1*f1 /\ 2*b1*f1 + f1 >= b1*d + 1 /\ f1 >= g1 /\ b1*d >= 2*b1*h1 /\ 2*b1*h1 + h1 >= b1*d + 1 /\ g1 >= h1 /\ c >= b1*d*i1 /\ b1*d*i1 + i1 >= c + 1 /\ c >= b1*d*j1 /\ b1*d*j1 + j1 >= c + 1 /\ b1*d*i1 >= 2*b1*j1*k1 /\ 2*b1*j1*k1 + k1 >= b1*d*i1 + 1 /\ k1 >= l1 /\ c >= b1*d*m1 /\ b1*d*m1 + m1 >= c + 1 /\ c >= b1*d*n1 /\ b1*d*n1 + n1 >= c + 1 /\ b1*d*m1 >= 2*b1*n1*o1 /\ 2*b1*n1*o1 + o1 >= b1*d*m1 + 1 /\ l1 >= o1 /\ b >= 1 /\ c >= b1*d*p1 /\ b1*d*p1 + p1 >= c + 1 /\ p1 >= q1 /\ c >= b1*d*r1 /\ b1*d*r1 + r1 >= c + 1 /\ q1 >= r1 ]
		(?, 1)    f19(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f23(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) [ h >= k /\ j >= k + 1 ]
		(?, 1)    f23(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f26(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) [ k + g >= l + 2 ]
		(?, 1)    f26(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f26(a, b, c, d, e, f, g, h, i, j, k, l, m + h, j + m - k, b1, p, q, r, s, t, u, v, w, x, y, z, a1) [ i >= m ]
		(?, 1)    f19(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f41(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, b1, q, r, s, t, u, v, w, x, y, z, a1) [ k >= j /\ h >= 2*q1 /\ 3*q1 >= h + 1 /\ q1 >= b1 /\ h >= 2*d1 /\ 3*d1 >= h + 1 /\ b1 >= d1 /\ h >= k ]
		(?, 1)    f41(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f41(a, b, c, d, e, f, g, h, i, j - p, k, l, m, n, o, b1, q, r, s, t, u, v, w, x, y, z, a1) [ j >= p + 1 /\ p >= 2*q1 /\ 3*q1 >= p + 1 /\ q1 >= b1 /\ p >= 2*d1 /\ 3*d1 >= p + 1 /\ b1 >= d1 /\ p >= g ]
		(?, 1)    f53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f63(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, 2*q, b1, q1, d1, g1, 1, 0, y, z, a1) [ h >= q + 1 ]
		(?, 1)    f63(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f66(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) [ q >= m ]
		(?, 1)    f66(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f69(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) [ m + g >= l + 2 ]
		(?, 1)    f69(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f69(a, b, c, d, e, f, g, h, i, j, k + r, l, m, n, b1*w - q1*x, p, q, r, s, t, u, v, w, x, k, k + q, d1*w + g1*x) [ i >= k ]
		(?, 1)    f69(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f66(a, b, c, d, e, f, g, h, i, j, k, l + 2, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) [ k >= i + 1 ]
		(?, 1)    f66(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f63(a, b, c, d, e, f, g, h, i, j, k, l, m + g, n, o, p, q, r, s, w, u, v, u*w - v*x + w, u*x + v*w + x, y, z, a1) [ l + 1 >= m + g ]
		(?, 1)    f63(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, r, r, s, t, u, v, w, x, y, z, a1) [ m >= q + 1 ]
		(?, 1)    f53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f10(a, b - 1, c, d*e, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) [ q >= h ]
		(?, 1)    f41(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f19(a, b, c, d, e, f, g, h, i, j + p, k + g, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) [ p >= g /\ p >= j ]
		(?, 1)    f41(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f19(a, b, c, d, e, f, g, h, i, j + p, k + g, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) [ g >= p + 1 ]
		(?, 1)    f26(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f23(a, b, c, d, e, f, g, h, i, j, k, l + 2, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) [ m >= i + 1 ]
		(?, 1)    f23(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f41(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, b1, q, r, s, t, u, v, w, x, y, z, a1) [ l + 1 >= k + g /\ h >= 2*q1 /\ 3*q1 >= h + 1 /\ q1 >= b1 /\ h >= 2*d1 /\ 3*d1 >= h + 1 /\ b1 >= d1 ]
		(?, 1)    f19(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, g, r, s, t, u, v, w, x, y, z, a1) [ k >= h + 1 ]
		(?, 1)    f10(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) [ 0 >= b ]
		(?, 1)    f2(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f10(a, b, c, 1, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) [ b >= a + 1 ]
		(1, 1)    start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f2(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1)
	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, g, h, i, j, k, l, m, p, q, r].
We thus obtain the following problem:
2:	T:
		(1, 1)    start(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f2(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r)
		(?, 1)    f2(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f10(a, b, c, 1, e, g, h, i, j, k, l, m, p, q, r) [ b >= a + 1 ]
		(?, 1)    f10(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f1(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) [ 0 >= b ]
		(?, 1)    f19(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f53(a, b, c, d, e, g, h, i, j, k, l, m, p, g, r) [ k >= h + 1 ]
		(?, 1)    f23(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f41(a, b, c, d, e, g, h, i, j, k, l, m, b1, q, r) [ l + 1 >= k + g /\ h >= 2*q1 /\ 3*q1 >= h + 1 /\ q1 >= b1 /\ h >= 2*d1 /\ 3*d1 >= h + 1 /\ b1 >= d1 ]
		(?, 1)    f26(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f23(a, b, c, d, e, g, h, i, j, k, l + 2, m, p, q, r) [ m >= i + 1 ]
		(?, 1)    f41(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f19(a, b, c, d, e, g, h, i, j + p, k + g, l, m, p, q, r) [ g >= p + 1 ]
		(?, 1)    f41(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f19(a, b, c, d, e, g, h, i, j + p, k + g, l, m, p, q, r) [ p >= g /\ p >= j ]
		(?, 1)    f53(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f10(a, b - 1, c, d*e, e, g, h, i, j, k, l, m, p, q, r) [ q >= h ]
		(?, 1)    f63(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f53(a, b, c, d, e, g, h, i, j, k, l, m, p, r, r) [ m >= q + 1 ]
		(?, 1)    f66(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f63(a, b, c, d, e, g, h, i, j, k, l, m + g, p, q, r) [ l + 1 >= m + g ]
		(?, 1)    f69(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f66(a, b, c, d, e, g, h, i, j, k, l + 2, m, p, q, r) [ k >= i + 1 ]
		(?, 1)    f69(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f69(a, b, c, d, e, g, h, i, j, k + r, l, m, p, q, r) [ i >= k ]
		(?, 1)    f66(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f69(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) [ m + g >= l + 2 ]
		(?, 1)    f63(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f66(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) [ q >= m ]
		(?, 1)    f53(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f63(a, b, c, d, e, g, h, i, j, k, l, m, p, q, 2*q) [ h >= q + 1 ]
		(?, 1)    f41(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f41(a, b, c, d, e, g, h, i, j - p, k, l, m, b1, q, r) [ j >= p + 1 /\ p >= 2*q1 /\ 3*q1 >= p + 1 /\ q1 >= b1 /\ p >= 2*d1 /\ 3*d1 >= p + 1 /\ b1 >= d1 /\ p >= g ]
		(?, 1)    f19(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f41(a, b, c, d, e, g, h, i, j, k, l, m, b1, q, r) [ k >= j /\ h >= 2*q1 /\ 3*q1 >= h + 1 /\ q1 >= b1 /\ h >= 2*d1 /\ 3*d1 >= h + 1 /\ b1 >= d1 /\ h >= k ]
		(?, 1)    f26(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f26(a, b, c, d, e, g, h, i, j, k, l, m + h, p, q, r) [ i >= m ]
		(?, 1)    f23(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f26(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) [ k + g >= l + 2 ]
		(?, 1)    f19(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f23(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) [ h >= k /\ j >= k + 1 ]
		(?, 1)    f10(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f19(a, b, c, d, b1, d1, g1, l1, 1, k, l, m, p, q, r) [ d >= 2*c1 /\ 3*c1 >= d + 1 /\ c1 >= d1 /\ d >= 2*e1 /\ 3*e1 >= d + 1 /\ d1 >= e1 /\ b1*d >= 2*b1*f1 /\ 2*b1*f1 + f1 >= b1*d + 1 /\ f1 >= g1 /\ b1*d >= 2*b1*h1 /\ 2*b1*h1 + h1 >= b1*d + 1 /\ g1 >= h1 /\ c >= b1*d*i1 /\ b1*d*i1 + i1 >= c + 1 /\ c >= b1*d*j1 /\ b1*d*j1 + j1 >= c + 1 /\ b1*d*i1 >= 2*b1*j1*k1 /\ 2*b1*j1*k1 + k1 >= b1*d*i1 + 1 /\ k1 >= l1 /\ c >= b1*d*m1 /\ b1*d*m1 + m1 >= c + 1 /\ c >= b1*d*n1 /\ b1*d*n1 + n1 >= c + 1 /\ b1*d*m1 >= 2*b1*n1*o1 /\ 2*b1*n1*o1 + o1 >= b1*d*m1 + 1 /\ l1 >= o1 /\ b >= 1 /\ c >= b1*d*p1 /\ b1*d*p1 + p1 >= c + 1 /\ p1 >= q1 /\ c >= b1*d*r1 /\ b1*d*r1 + r1 >= c + 1 /\ q1 >= r1 ]
		(?, 1)    f2(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f2(a, b + 1, b1*c, d, e, g, h, i, j, k, l, m, p, q, r) [ a >= b ]
	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, g, h, i, j, k, l, m, p, q, r) -> f2(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r)
		(?, 1)    f19(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f53(a, b, c, d, e, g, h, i, j, k, l, m, p, g, r) [ k >= h + 1 ]
		(?, 1)    f23(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f41(a, b, c, d, e, g, h, i, j, k, l, m, b1, q, r) [ l + 1 >= k + g /\ h >= 2*q1 /\ 3*q1 >= h + 1 /\ q1 >= b1 /\ h >= 2*d1 /\ 3*d1 >= h + 1 /\ b1 >= d1 ]
		(?, 1)    f26(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f23(a, b, c, d, e, g, h, i, j, k, l + 2, m, p, q, r) [ m >= i + 1 ]
		(?, 1)    f41(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f19(a, b, c, d, e, g, h, i, j + p, k + g, l, m, p, q, r) [ g >= p + 1 ]
		(?, 1)    f41(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f19(a, b, c, d, e, g, h, i, j + p, k + g, l, m, p, q, r) [ p >= g /\ p >= j ]
		(?, 1)    f53(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f10(a, b - 1, c, d*e, e, g, h, i, j, k, l, m, p, q, r) [ q >= h ]
		(?, 1)    f63(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f53(a, b, c, d, e, g, h, i, j, k, l, m, p, r, r) [ m >= q + 1 ]
		(?, 1)    f66(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f63(a, b, c, d, e, g, h, i, j, k, l, m + g, p, q, r) [ l + 1 >= m + g ]
		(?, 1)    f69(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f66(a, b, c, d, e, g, h, i, j, k, l + 2, m, p, q, r) [ k >= i + 1 ]
		(?, 1)    f69(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f69(a, b, c, d, e, g, h, i, j, k + r, l, m, p, q, r) [ i >= k ]
		(?, 1)    f66(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f69(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) [ m + g >= l + 2 ]
		(?, 1)    f63(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f66(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) [ q >= m ]
		(?, 1)    f53(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f63(a, b, c, d, e, g, h, i, j, k, l, m, p, q, 2*q) [ h >= q + 1 ]
		(?, 1)    f41(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f41(a, b, c, d, e, g, h, i, j - p, k, l, m, b1, q, r) [ j >= p + 1 /\ p >= 2*q1 /\ 3*q1 >= p + 1 /\ q1 >= b1 /\ p >= 2*d1 /\ 3*d1 >= p + 1 /\ b1 >= d1 /\ p >= g ]
		(?, 1)    f19(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f41(a, b, c, d, e, g, h, i, j, k, l, m, b1, q, r) [ k >= j /\ h >= 2*q1 /\ 3*q1 >= h + 1 /\ q1 >= b1 /\ h >= 2*d1 /\ 3*d1 >= h + 1 /\ b1 >= d1 /\ h >= k ]
		(?, 1)    f26(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f26(a, b, c, d, e, g, h, i, j, k, l, m + h, p, q, r) [ i >= m ]
		(?, 1)    f23(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f26(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) [ k + g >= l + 2 ]
		(?, 1)    f19(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f23(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) [ h >= k /\ j >= k + 1 ]
		(?, 1)    f10(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f19(a, b, c, d, b1, d1, g1, l1, 1, k, l, m, p, q, r) [ d >= 2*c1 /\ 3*c1 >= d + 1 /\ c1 >= d1 /\ d >= 2*e1 /\ 3*e1 >= d + 1 /\ d1 >= e1 /\ b1*d >= 2*b1*f1 /\ 2*b1*f1 + f1 >= b1*d + 1 /\ f1 >= g1 /\ b1*d >= 2*b1*h1 /\ 2*b1*h1 + h1 >= b1*d + 1 /\ g1 >= h1 /\ c >= b1*d*i1 /\ b1*d*i1 + i1 >= c + 1 /\ c >= b1*d*j1 /\ b1*d*j1 + j1 >= c + 1 /\ b1*d*i1 >= 2*b1*j1*k1 /\ 2*b1*j1*k1 + k1 >= b1*d*i1 + 1 /\ k1 >= l1 /\ c >= b1*d*m1 /\ b1*d*m1 + m1 >= c + 1 /\ c >= b1*d*n1 /\ b1*d*n1 + n1 >= c + 1 /\ b1*d*m1 >= 2*b1*n1*o1 /\ 2*b1*n1*o1 + o1 >= b1*d*m1 + 1 /\ l1 >= o1 /\ b >= 1 /\ c >= b1*d*p1 /\ b1*d*p1 + p1 >= c + 1 /\ p1 >= q1 /\ c >= b1*d*r1 /\ b1*d*r1 + r1 >= c + 1 /\ q1 >= r1 ]
		(?, 1)    f2(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f2(a, b + 1, b1*c, d, e, g, h, i, j, k, l, m, p, q, r) [ a >= b ]
	start location:	start
	leaf cost:	2

Testing for reachability in the complexity graph removes the following transitions from problem 3:
	f19(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f53(a, b, c, d, e, g, h, i, j, k, l, m, p, g, r) [ k >= h + 1 ]
	f23(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f41(a, b, c, d, e, g, h, i, j, k, l, m, b1, q, r) [ l + 1 >= k + g /\ h >= 2*q1 /\ 3*q1 >= h + 1 /\ q1 >= b1 /\ h >= 2*d1 /\ 3*d1 >= h + 1 /\ b1 >= d1 ]
	f26(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f23(a, b, c, d, e, g, h, i, j, k, l + 2, m, p, q, r) [ m >= i + 1 ]
	f41(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f19(a, b, c, d, e, g, h, i, j + p, k + g, l, m, p, q, r) [ g >= p + 1 ]
	f41(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f19(a, b, c, d, e, g, h, i, j + p, k + g, l, m, p, q, r) [ p >= g /\ p >= j ]
	f53(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f10(a, b - 1, c, d*e, e, g, h, i, j, k, l, m, p, q, r) [ q >= h ]
	f63(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f53(a, b, c, d, e, g, h, i, j, k, l, m, p, r, r) [ m >= q + 1 ]
	f66(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f63(a, b, c, d, e, g, h, i, j, k, l, m + g, p, q, r) [ l + 1 >= m + g ]
	f69(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f66(a, b, c, d, e, g, h, i, j, k, l + 2, m, p, q, r) [ k >= i + 1 ]
	f69(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f69(a, b, c, d, e, g, h, i, j, k + r, l, m, p, q, r) [ i >= k ]
	f66(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f69(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) [ m + g >= l + 2 ]
	f63(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f66(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) [ q >= m ]
	f53(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f63(a, b, c, d, e, g, h, i, j, k, l, m, p, q, 2*q) [ h >= q + 1 ]
	f41(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f41(a, b, c, d, e, g, h, i, j - p, k, l, m, b1, q, r) [ j >= p + 1 /\ p >= 2*q1 /\ 3*q1 >= p + 1 /\ q1 >= b1 /\ p >= 2*d1 /\ 3*d1 >= p + 1 /\ b1 >= d1 /\ p >= g ]
	f19(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f41(a, b, c, d, e, g, h, i, j, k, l, m, b1, q, r) [ k >= j /\ h >= 2*q1 /\ 3*q1 >= h + 1 /\ q1 >= b1 /\ h >= 2*d1 /\ 3*d1 >= h + 1 /\ b1 >= d1 /\ h >= k ]
	f26(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f26(a, b, c, d, e, g, h, i, j, k, l, m + h, p, q, r) [ i >= m ]
	f23(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f26(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) [ k + g >= l + 2 ]
	f19(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f23(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) [ h >= k /\ j >= k + 1 ]
	f10(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f19(a, b, c, d, b1, d1, g1, l1, 1, k, l, m, p, q, r) [ d >= 2*c1 /\ 3*c1 >= d + 1 /\ c1 >= d1 /\ d >= 2*e1 /\ 3*e1 >= d + 1 /\ d1 >= e1 /\ b1*d >= 2*b1*f1 /\ 2*b1*f1 + f1 >= b1*d + 1 /\ f1 >= g1 /\ b1*d >= 2*b1*h1 /\ 2*b1*h1 + h1 >= b1*d + 1 /\ g1 >= h1 /\ c >= b1*d*i1 /\ b1*d*i1 + i1 >= c + 1 /\ c >= b1*d*j1 /\ b1*d*j1 + j1 >= c + 1 /\ b1*d*i1 >= 2*b1*j1*k1 /\ 2*b1*j1*k1 + k1 >= b1*d*i1 + 1 /\ k1 >= l1 /\ c >= b1*d*m1 /\ b1*d*m1 + m1 >= c + 1 /\ c >= b1*d*n1 /\ b1*d*n1 + n1 >= c + 1 /\ b1*d*m1 >= 2*b1*n1*o1 /\ 2*b1*n1*o1 + o1 >= b1*d*m1 + 1 /\ l1 >= o1 /\ b >= 1 /\ c >= b1*d*p1 /\ b1*d*p1 + p1 >= c + 1 /\ p1 >= q1 /\ c >= b1*d*r1 /\ b1*d*r1 + r1 >= c + 1 /\ q1 >= r1 ]
We thus obtain the following problem:
4:	T:
		(?, 1)    f2(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f2(a, b + 1, b1*c, d, e, g, h, i, j, k, l, m, p, q, r) [ a >= b ]
		(1, 1)    start(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f2(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r)
	start location:	start
	leaf cost:	2

A polynomial rank function with
	Pol(f2) = V_1 - V_2 + 1
	Pol(start) = V_1 - V_2 + 1
orients all transitions weakly and the transition
	f2(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f2(a, b + 1, b1*c, d, e, g, h, i, j, k, l, m, p, q, r) [ a >= b ]
strictly and produces the following problem:
5:	T:
		(a + b + 1, 1)    f2(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f2(a, b + 1, b1*c, d, e, g, h, i, j, k, l, m, p, q, r) [ a >= b ]
		(1, 1)            start(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r) -> f2(a, b, c, d, e, g, h, i, j, k, l, m, p, q, r)
	start location:	start
	leaf cost:	2

Complexity upper bound a + b + 4

Time: 0.413 sec (SMT: 0.361 sec)