MAYBE

Initial complexity problem:
1:	T:
		(?, 1)    f15(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f15(a, b + 1, d, x1, d, y1, b, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ a >= b + 1 /\ b >= 0 ]
		(?, 1)    f13(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f13(a, b, c, d, e, f, g, h + 1, i - 1, x1, y1, a2, a2, c2, d2, 0, e2, f2, g2, h2, i2, j2, 0, k2, z, z, b2, h + 1, i - 1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f13(a, b, c, d, e, f, g, h + 1, i - 1, x1, y1, a2, a2, c2, d2, 0, e2, f2, g2, h2, i2, j2, 0, k2, z, z, b2, h + 1, i - 1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
		(?, 1)    f13(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f13(a, b, c, d, e, f, g, h + 1, i - 1, x1, y1, a2, a2, c2, d2, 0, e2, f2, g2, h2, i2, j2, 0, k2, z, z, b2, h + 1, i - 1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f13(a, b, c, d, e, f, g, h + 1, i - 1, x1, y1, a2, a2, c2, d2, 0, e2, f2, g2, h2, i2, j2, 0, k2, z, z, b2, h + 1, i - 1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ b2 >= 1 ]
		(?, 1)    f13(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f13(a, b, c, d, e, f, g, h + 1, i - 1, x1, y1, a2, a2, c2, d2, 0, e2, f2, g2, h2, i2, j2, 0, k2, z, z, b2, h + 1, i - 1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f13(a, b, c, d, e, f, g, h + 1, i - 1, x1, y1, a2, a2, c2, d2, 0, e2, f2, g2, h2, i2, j2, 0, k2, z, z, b2, h + 1, i - 1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
		(?, 1)    f13(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f13(a, b, c, d, e, f, g, h + 1, i - 1, x1, y1, a2, a2, c2, d2, 0, e2, f2, g2, h2, i2, j2, 0, k2, z, z, b2, h + 1, i - 1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f13(a, b, c, d, e, f, g, h + 1, i - 1, x1, y1, a2, a2, c2, d2, 0, e2, f2, g2, h2, i2, j2, 0, k2, z, z, b2, h + 1, i - 1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ b2 >= 1 ]
		(?, 1)    f9(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f10(a, b, c, d, e, f, g, h, i, x1, k, y1, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, 0, y1, 0, y1, d1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ a2 >= d1 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ y1 >= a2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f9(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f10(a, b, c, d, e, f, g, h, i, x1, k, y1, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, 0, y1, 0, y1, d1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ a2 >= d1 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ y1 >= a2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f9(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f10(a, b, c, d, e, f, g, h, i, x1, k, y1, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, 0, y1, 0, y1, d1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ a2 >= d1 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ a2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f9(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f10(a, b, c, d, e, f, g, h, i, x1, k, y1, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, 0, y1, 0, y1, d1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ a2 >= d1 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ a2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f9(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f10(a, b, c, d, e, f, g, h, i, x1, k, y1, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, 0, y1, 0, y1, d1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ d1 >= a2 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ y1 >= a2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f9(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f10(a, b, c, d, e, f, g, h, i, x1, k, y1, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, 0, y1, 0, y1, d1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ d1 >= a2 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ y1 >= a2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f9(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f10(a, b, c, d, e, f, g, h, i, x1, k, y1, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, 0, y1, 0, y1, d1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ d1 >= a2 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ a2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f9(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f10(a, b, c, d, e, f, g, h, i, x1, k, y1, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, 0, y1, 0, y1, d1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ d1 >= a2 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ a2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f9(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f0(a, b, c, d, e, f, g, h, i, x1, y1, a2, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, g2, e1, f2, c2, d2, e2, h2, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ e1 >= 0 /\ 0 >= a2 + 1 /\ x1 >= 2 /\ f1 = d1 ]
		(?, 1)    f9(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f0(a, b, c, d, e, f, g, h, i, x1, y1, a2, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, g2, e1, f2, c2, d2, e2, h2, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ e1 >= 0 /\ a2 >= 1 /\ x1 >= 2 /\ f1 = d1 ]
		(?, 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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f10(a, b, c, d, e, f, g, h, i, x1, k, y1, m, n, o, p, q, r, s, t, u, v, w, a2, y, z, a1, b1, c1, d1, e1, 0, y1, 0, y1, d1, k1 - 1, k1 - 1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f10(a, b, c, d, e, f, g, h, i, x1, k, y1, m, n, o, p, q, r, s, t, u, v, w, a2, y, z, a1, b1, c1, d1, e1, 0, y1, 0, y1, d1, k1 - 1, k1 - 1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f10(a, b, c, d, e, f, g, h, i, x1, k, y1, m, n, o, p, q, r, s, t, u, v, w, a2, y, z, a1, b1, c1, d1, e1, 0, y1, 0, y1, d1, k1 - 1, k1 - 1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f10(a, b, c, d, e, f, g, h, i, x1, k, y1, m, n, o, p, q, r, s, t, u, v, w, a2, y, z, a1, b1, c1, d1, e1, 0, y1, 0, y1, d1, k1 - 1, k1 - 1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f10(a, b, c, d, e, f, g, h, i, x1, k, y1, m, n, o, p, q, r, s, t, u, v, w, a2, y, z, a1, b1, c1, d1, e1, 0, y1, 0, y1, d1, k1 - 1, k1 - 1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f10(a, b, c, d, e, f, g, h, i, x1, k, y1, m, n, o, p, q, r, s, t, u, v, w, a2, y, z, a1, b1, c1, d1, e1, 0, y1, 0, y1, d1, k1 - 1, k1 - 1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f10(a, b, c, d, e, f, g, h, i, x1, k, y1, m, n, o, p, q, r, s, t, u, v, w, a2, y, z, a1, b1, c1, d1, e1, 0, y1, 0, y1, d1, k1 - 1, k1 - 1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f10(a, b, c, d, e, f, g, h, i, x1, k, y1, m, n, o, p, q, r, s, t, u, v, w, a2, y, z, a1, b1, c1, d1, e1, 0, y1, 0, y1, d1, k1 - 1, k1 - 1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f0(a, b, c, d, e, f, g, h, i, x1, y1, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, f2, e1, e2, a2, c2, d2, g2, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) [ x1 >= 2 /\ k1 >= 0 /\ f1 = d1 ]
		(1, 1)    f17(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f15(y1, 2, a2, c2, a2, f, g, h, i, y1, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, x1, a2, d2, p1, q1, r1, s1, t1, u1, v1, w1) [ y1 >= 2 ]
		(?, 1)    f15(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f13(y1, c2, a2, h2, g2, f, g, h, i, x1, e2, i2, i2, k2, b2, 0, n2, o2, p2, q2, r2, s2, 0, x, y, c, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, f2, o1, p1, d2, j2, z1, t2, m2, v1, w1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
		(?, 1)    f15(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f13(y1, c2, a2, h2, g2, f, g, h, i, x1, e2, i2, i2, k2, b2, 0, n2, o2, p2, q2, r2, s2, 0, x, y, c, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, f2, o1, p1, d2, j2, z1, t2, m2, v1, w1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
		(?, 1)    f15(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f13(y1, c2, a2, h2, g2, f, g, h, i, x1, e2, i2, i2, k2, b2, 0, n2, o2, p2, q2, r2, s2, 0, x, y, c, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, f2, o1, p1, d2, j2, z1, t2, m2, v1, w1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
		(?, 1)    f15(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f13(y1, c2, a2, h2, g2, f, g, h, i, x1, e2, i2, i2, k2, b2, 0, n2, o2, p2, q2, r2, s2, 0, x, y, c, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, f2, o1, p1, d2, j2, z1, t2, m2, v1, w1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ i2 >= 1 ]
		(?, 1)    f15(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f13(y1, c2, a2, h2, g2, f, g, h, i, x1, e2, i2, i2, k2, b2, 0, n2, o2, p2, q2, r2, s2, 0, x, y, c, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, f2, o1, p1, d2, j2, z1, t2, m2, v1, w1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
		(?, 1)    f15(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f13(y1, c2, a2, h2, g2, f, g, h, i, x1, e2, i2, i2, k2, b2, 0, n2, o2, p2, q2, r2, s2, 0, x, y, c, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, f2, o1, p1, d2, j2, z1, t2, m2, v1, w1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
		(?, 1)    f15(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f13(y1, c2, a2, h2, g2, f, g, h, i, x1, e2, i2, i2, k2, b2, 0, n2, o2, p2, q2, r2, s2, 0, x, y, c, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, f2, o1, p1, d2, j2, z1, t2, m2, v1, w1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
		(?, 1)    f15(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f13(y1, c2, a2, h2, g2, f, g, h, i, x1, e2, i2, i2, k2, b2, 0, n2, o2, p2, q2, r2, s2, 0, x, y, c, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, f2, o1, p1, d2, j2, z1, t2, m2, v1, w1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ i2 >= 1 ]
		(1, 1)    f17(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f0(a2, d2, c2, i2, h2, f, g, h, i, y1, f2, 0, j2, z1, n2, o2, p2, q2, r2, s2, t2, w2, x2, x, y, k2, a1, b1, c1, c3, e1, b3, y2, z2, a3, d3, k1, l1, x1, g2, o1, p1, e2, b2, s1, t1, u1, m2, l2) [ 0 >= u2 /\ 0 >= y1 /\ 0 >= v2 ]
		(?, 1)    f13(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f10(a, b, c, d, e, f, g, k1 + 1, i, x1, y1, l, a2, e2, f2, g2, h2, i2, j2, k2, b2, o2, p2, x, y, c2, a1, b1, c1, l, k1, 0, l, 0, l, l, k1, l1, m1, n1, o1, p1, q1, d2, s1, t1, u1, z1, n2) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ l >= 1 /\ 0 >= l + 1 /\ z = 0 ]
		(?, 1)    f13(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f10(a, b, c, d, e, f, g, k1 + 1, i, x1, y1, l, a2, e2, f2, g2, h2, i2, j2, k2, b2, o2, p2, x, y, c2, a1, b1, c1, l, k1, 0, l, 0, l, l, k1, l1, m1, n1, o1, p1, q1, d2, s1, t1, u1, z1, n2) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ l >= 1 /\ z = 0 ]
		(?, 1)    f13(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f10(a, b, c, d, e, f, g, k1 + 1, i, x1, y1, l, a2, e2, f2, g2, h2, i2, j2, k2, b2, o2, p2, x, y, c2, a1, b1, c1, l, k1, 0, l, 0, l, l, k1, l1, m1, n1, o1, p1, q1, d2, s1, t1, u1, z1, n2) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ 0 >= l + 1 /\ z = 0 ]
		(?, 1)    f13(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, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1) -> f10(a, b, c, d, e, f, g, k1 + 1, i, x1, y1, l, a2, e2, f2, g2, h2, i2, j2, k2, b2, o2, p2, x, y, c2, a1, b1, c1, l, k1, 0, l, 0, l, l, k1, l1, m1, n1, o1, p1, q1, d2, s1, t1, u1, z1, n2) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ 0 >= l + 1 /\ l >= 1 /\ z = 0 ]
	start location:	f17
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1].
We thus obtain the following problem:
2:	T:
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ 0 >= l + 1 /\ l >= 1 /\ z = 0 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ 0 >= l + 1 /\ z = 0 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ l >= 1 /\ z = 0 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ l >= 1 /\ 0 >= l + 1 /\ z = 0 ]
		(1, 1)    f17(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f0(a2, d2, c2, i2, h, i, 0, k2, c3, e1, b3, k1, p1) [ 0 >= u2 /\ 0 >= y1 /\ 0 >= v2 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ i2 >= 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ i2 >= 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
		(1, 1)    f17(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f15(y1, 2, a2, c2, h, i, l, z, d1, e1, f1, k1, p1) [ y1 >= 2 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f0(a, b, c, d, h, i, l, z, f2, e1, e2, k1, p1) [ x1 >= 2 /\ k1 >= 0 /\ f1 = d1 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f0(a, b, c, d, h, i, a2, z, g2, e1, f2, k1, p1) [ e1 >= 0 /\ a2 >= 1 /\ x1 >= 2 /\ f1 = d1 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f0(a, b, c, d, h, i, a2, z, g2, e1, f2, k1, p1) [ e1 >= 0 /\ 0 >= a2 + 1 /\ x1 >= 2 /\ f1 = d1 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ d1 >= a2 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ a2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ d1 >= a2 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ a2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ d1 >= a2 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ y1 >= a2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ d1 >= a2 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ y1 >= a2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ a2 >= d1 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ a2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ a2 >= d1 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ a2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ a2 >= d1 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ y1 >= a2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ a2 >= d1 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ y1 >= a2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f15(a, b + 1, d, x1, h, i, l, z, d1, e1, f1, k1, p1) [ a >= b + 1 /\ b >= 0 ]
	start location:	f17
	leaf cost:	0

Testing for unsatisfiable constraints removes the following transitions from problem 2:
	f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ 0 >= l + 1 /\ l >= 1 /\ z = 0 ]
	f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ l >= 1 /\ 0 >= l + 1 /\ z = 0 ]
We thus obtain the following problem:
3:	T:
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ 0 >= l + 1 /\ z = 0 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ l >= 1 /\ z = 0 ]
		(1, 1)    f17(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f0(a2, d2, c2, i2, h, i, 0, k2, c3, e1, b3, k1, p1) [ 0 >= u2 /\ 0 >= y1 /\ 0 >= v2 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ i2 >= 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ i2 >= 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
		(1, 1)    f17(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f15(y1, 2, a2, c2, h, i, l, z, d1, e1, f1, k1, p1) [ y1 >= 2 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f0(a, b, c, d, h, i, l, z, f2, e1, e2, k1, p1) [ x1 >= 2 /\ k1 >= 0 /\ f1 = d1 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f0(a, b, c, d, h, i, a2, z, g2, e1, f2, k1, p1) [ e1 >= 0 /\ a2 >= 1 /\ x1 >= 2 /\ f1 = d1 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f0(a, b, c, d, h, i, a2, z, g2, e1, f2, k1, p1) [ e1 >= 0 /\ 0 >= a2 + 1 /\ x1 >= 2 /\ f1 = d1 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ d1 >= a2 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ a2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ d1 >= a2 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ a2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ d1 >= a2 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ y1 >= a2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ d1 >= a2 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ y1 >= a2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ a2 >= d1 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ a2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ a2 >= d1 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ a2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ a2 >= d1 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ y1 >= a2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ a2 >= d1 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ y1 >= a2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f15(a, b + 1, d, x1, h, i, l, z, d1, e1, f1, k1, p1) [ a >= b + 1 /\ b >= 0 ]
	start location:	f17
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 3 produces the following problem:
4:	T:
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ 0 >= l + 1 /\ z = 0 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ l >= 1 /\ z = 0 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ i2 >= 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ i2 >= 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
		(1, 1)    f17(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f15(y1, 2, a2, c2, h, i, l, z, d1, e1, f1, k1, p1) [ y1 >= 2 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ d1 >= a2 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ a2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ d1 >= a2 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ a2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ d1 >= a2 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ y1 >= a2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ d1 >= a2 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ y1 >= a2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ a2 >= d1 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ a2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ a2 >= d1 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ a2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ a2 >= d1 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ y1 >= a2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ a2 >= d1 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ y1 >= a2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f15(a, b + 1, d, x1, h, i, l, z, d1, e1, f1, k1, p1) [ a >= b + 1 /\ b >= 0 ]
	start location:	f17
	leaf cost:	4

Testing for reachability in the complexity graph removes the following transitions from problem 4:
	f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ d1 >= a2 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ a2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
	f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ d1 >= a2 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ a2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
	f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ d1 >= a2 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ y1 >= a2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
	f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ d1 >= a2 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ y1 >= a2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
	f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ a2 >= d1 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ a2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
	f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ a2 >= d1 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ a2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
	f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ a2 >= d1 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ y1 >= a2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
	f9(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1, p1) [ a2 >= d1 + 1 /\ e1 >= 0 /\ x1 >= 2 /\ y1 >= a2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
We thus obtain the following problem:
5:	T:
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ 0 >= l + 1 /\ z = 0 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ l >= 1 /\ z = 0 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ b2 >= 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f15(a, b + 1, d, x1, h, i, l, z, d1, e1, f1, k1, p1) [ a >= b + 1 /\ b >= 0 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ i2 >= 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ i2 >= 1 ]
		(1, 1)    f17(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f15(y1, 2, a2, c2, h, i, l, z, d1, e1, f1, k1, p1) [ y1 >= 2 ]
	start location:	f17
	leaf cost:	4

A polynomial rank function with
	Pol(f10) = -8
	Pol(f13) = -5
	Pol(f15) = 2
	Pol(f17) = 2
orients all transitions weakly and the transitions
	f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ i2 >= 1 ]
	f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
	f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
	f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
	f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ i2 >= 1 ]
	f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
	f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
	f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
strictly and produces the following problem:
6:	T:
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ 0 >= l + 1 /\ z = 0 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ l >= 1 /\ z = 0 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ b2 >= 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f15(a, b + 1, d, x1, h, i, l, z, d1, e1, f1, k1, p1) [ a >= b + 1 /\ b >= 0 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ i2 >= 1 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ i2 >= 1 ]
		(1, 1)    f17(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f15(y1, 2, a2, c2, h, i, l, z, d1, e1, f1, k1, p1) [ y1 >= 2 ]
	start location:	f17
	leaf cost:	4

A polynomial rank function with
	Pol(f10) = -8
	Pol(f13) = 1
	Pol(f15) = 1
	Pol(f17) = 1
orients all transitions weakly and the transition
	f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ l >= 1 /\ z = 0 ]
strictly and produces the following problem:
7:	T:
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ 0 >= l + 1 /\ z = 0 ]
		(1, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ l >= 1 /\ z = 0 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ b2 >= 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f15(a, b + 1, d, x1, h, i, l, z, d1, e1, f1, k1, p1) [ a >= b + 1 /\ b >= 0 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ i2 >= 1 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ i2 >= 1 ]
		(1, 1)    f17(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f15(y1, 2, a2, c2, h, i, l, z, d1, e1, f1, k1, p1) [ y1 >= 2 ]
	start location:	f17
	leaf cost:	4

A polynomial rank function with
	Pol(f10) = -8
	Pol(f13) = 1
	Pol(f15) = 1
	Pol(f17) = 1
orients all transitions weakly and the transition
	f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ 0 >= l + 1 /\ z = 0 ]
strictly and produces the following problem:
8:	T:
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(1, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ 0 >= l + 1 /\ z = 0 ]
		(1, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ l >= 1 /\ z = 0 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
		(?, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ b2 >= 1 ]
		(?, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f15(a, b + 1, d, x1, h, i, l, z, d1, e1, f1, k1, p1) [ a >= b + 1 /\ b >= 0 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ i2 >= 1 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
		(2, 1)    f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ i2 >= 1 ]
		(1, 1)    f17(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f15(y1, 2, a2, c2, h, i, l, z, d1, e1, f1, k1, p1) [ y1 >= 2 ]
	start location:	f17
	leaf cost:	4

A polynomial rank function with
	Pol(f10) = -2*V_5 - V_6 + V_10 + V_12 - 8
	Pol(f13) = V_5 + 2*V_6 + 1
	Pol(f15) = V_5 + 2*V_6 + V_13 + 1
	Pol(f17) = V_5 + 2*V_6 + V_13 + 1
orients all transitions weakly and the transitions
	f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ b2 >= 1 ]
	f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
	f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
	f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
	f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ b2 >= 1 ]
	f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
	f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
	f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
strictly and produces the following problem:
9:	T:
		(?, 1)                   f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)                   f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)                   f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)                   f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)                   f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)                   f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(?, 1)                   f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(?, 1)                   f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(1, 1)                   f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ 0 >= l + 1 /\ z = 0 ]
		(1, 1)                   f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ l >= 1 /\ z = 0 ]
		(h + 2*i + p1 + 1, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
		(h + 2*i + p1 + 1, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
		(h + 2*i + p1 + 1, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
		(h + 2*i + p1 + 1, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ b2 >= 1 ]
		(h + 2*i + p1 + 1, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
		(h + 2*i + p1 + 1, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
		(h + 2*i + p1 + 1, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
		(h + 2*i + p1 + 1, 1)    f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ b2 >= 1 ]
		(?, 1)                   f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f15(a, b + 1, d, x1, h, i, l, z, d1, e1, f1, k1, p1) [ a >= b + 1 /\ b >= 0 ]
		(2, 1)                   f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
		(2, 1)                   f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
		(2, 1)                   f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
		(2, 1)                   f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ i2 >= 1 ]
		(2, 1)                   f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
		(2, 1)                   f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
		(2, 1)                   f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
		(2, 1)                   f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ i2 >= 1 ]
		(1, 1)                   f17(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f15(y1, 2, a2, c2, h, i, l, z, d1, e1, f1, k1, p1) [ y1 >= 2 ]
	start location:	f17
	leaf cost:	4

A polynomial rank function with
	Pol(f10) = V_12 + 1
	Pol(f13) = V_5 + V_6 + V_12 + 1
	Pol(f15) = V_5 + V_6 + V_12 + V_13 + 1
	Pol(f17) = V_5 + V_6 + V_12 + V_13 + 1
orients all transitions weakly and the transitions
	f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
	f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
	f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
	f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
	f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
	f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
	f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
	f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
strictly and produces the following problem:
10:	T:
		(h + i + k1 + p1 + 1, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(h + i + k1 + p1 + 1, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(h + i + k1 + p1 + 1, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(h + i + k1 + p1 + 1, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(h + i + k1 + p1 + 1, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(h + i + k1 + p1 + 1, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(h + i + k1 + p1 + 1, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(h + i + k1 + p1 + 1, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(1, 1)                      f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ 0 >= l + 1 /\ z = 0 ]
		(1, 1)                      f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ l >= 1 /\ z = 0 ]
		(h + 2*i + p1 + 1, 1)       f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
		(h + 2*i + p1 + 1, 1)       f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
		(h + 2*i + p1 + 1, 1)       f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
		(h + 2*i + p1 + 1, 1)       f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ b2 >= 1 ]
		(h + 2*i + p1 + 1, 1)       f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
		(h + 2*i + p1 + 1, 1)       f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
		(h + 2*i + p1 + 1, 1)       f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
		(h + 2*i + p1 + 1, 1)       f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ b2 >= 1 ]
		(?, 1)                      f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f15(a, b + 1, d, x1, h, i, l, z, d1, e1, f1, k1, p1) [ a >= b + 1 /\ b >= 0 ]
		(2, 1)                      f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
		(2, 1)                      f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
		(2, 1)                      f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
		(2, 1)                      f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ i2 >= 1 ]
		(2, 1)                      f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
		(2, 1)                      f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
		(2, 1)                      f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
		(2, 1)                      f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ i2 >= 1 ]
		(1, 1)                      f17(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f15(y1, 2, a2, c2, h, i, l, z, d1, e1, f1, k1, p1) [ y1 >= 2 ]
	start location:	f17
	leaf cost:	4

Applied AI with 'oct' on problem 10 to obtain the following invariants:
  For symbol f10: X_6 >= 0 /\ X_13 + X_6 >= 0 /\ X_11 + X_6 >= 0 /\ -X_11 + X_6 >= 0 /\ X_10 - X_5 + 1 >= 0 /\ -X_12 + X_5 - 1 >= 0 /\ -X_10 + X_5 - 1 >= 0 /\ X_13 >= 0 /\ X_11 + X_13 >= 0 /\ -X_11 + X_13 >= 0 /\ X_10 - X_12 >= 0 /\ -X_11 >= 0 /\ X_11 >= 0
  For symbol f13: X_13 >= 0
  For symbol f15: X_1 - X_2 >= 0 /\ X_2 - 2 >= 0 /\ X_1 + X_2 - 4 >= 0 /\ X_1 - 2 >= 0


This yielded the following problem:
11:	T:
		(1, 1)                      f17(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f15(y1, 2, a2, c2, h, i, l, z, d1, e1, f1, k1, p1) [ y1 >= 2 ]
		(2, 1)                      f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ i2 >= 1 ]
		(2, 1)                      f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
		(2, 1)                      f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
		(2, 1)                      f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ m2 >= 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
		(2, 1)                      f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ i2 >= 1 ]
		(2, 1)                      f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ c >= 1 /\ 0 >= i2 + 1 ]
		(2, 1)                      f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ i2 >= 1 ]
		(2, 1)                      f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(y1, c2, a2, h2, h, i, i2, c, d1, e1, f1, k1, p1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ l2 >= 2 /\ z1 >= l2 /\ x1 >= 2 /\ b >= a /\ b >= 0 /\ p1 >= 0 /\ 0 >= m2 + 1 /\ 0 >= c + 1 /\ 0 >= i2 + 1 ]
		(?, 1)                      f15(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f15(a, b + 1, d, x1, h, i, l, z, d1, e1, f1, k1, p1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ]
		(h + 2*i + p1 + 1, 1)       f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ p1 >= 0 /\ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ b2 >= 1 ]
		(h + 2*i + p1 + 1, 1)       f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ p1 >= 0 /\ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
		(h + 2*i + p1 + 1, 1)       f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ p1 >= 0 /\ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
		(h + 2*i + p1 + 1, 1)       f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ p1 >= 0 /\ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ z1 >= 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
		(h + 2*i + p1 + 1, 1)       f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ p1 >= 0 /\ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ b2 >= 1 ]
		(h + 2*i + p1 + 1, 1)       f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ p1 >= 0 /\ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ a2 >= 1 /\ 0 >= b2 + 1 ]
		(h + 2*i + p1 + 1, 1)       f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ p1 >= 0 /\ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ b2 >= 1 ]
		(h + 2*i + p1 + 1, 1)       f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f13(a, b, c, d, h + 1, i - 1, a2, z, d1, e1, f1, k1, p1) [ p1 >= 0 /\ h >= 0 /\ i >= 0 /\ x1 >= 2 /\ 0 >= z1 + 1 /\ 0 >= a2 + 1 /\ 0 >= b2 + 1 ]
		(1, 1)                      f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ p1 >= 0 /\ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ l >= 1 /\ z = 0 ]
		(1, 1)                      f13(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, k1 + 1, i, l, c2, l, k1, 0, k1, p1) [ p1 >= 0 /\ q2 >= 2 /\ x1 >= 2 /\ i >= 0 /\ h >= 0 /\ 0 >= l + 1 /\ z = 0 ]
		(h + i + k1 + p1 + 1, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ i >= 0 /\ p1 + i >= 0 /\ f1 + i >= 0 /\ -f1 + i >= 0 /\ e1 - h + 1 >= 0 /\ -k1 + h - 1 >= 0 /\ -e1 + h - 1 >= 0 /\ p1 >= 0 /\ f1 + p1 >= 0 /\ -f1 + p1 >= 0 /\ e1 - k1 >= 0 /\ -f1 >= 0 /\ f1 >= 0 /\ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(h + i + k1 + p1 + 1, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ i >= 0 /\ p1 + i >= 0 /\ f1 + i >= 0 /\ -f1 + i >= 0 /\ e1 - h + 1 >= 0 /\ -k1 + h - 1 >= 0 /\ -e1 + h - 1 >= 0 /\ p1 >= 0 /\ f1 + p1 >= 0 /\ -f1 + p1 >= 0 /\ e1 - k1 >= 0 /\ -f1 >= 0 /\ f1 >= 0 /\ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(h + i + k1 + p1 + 1, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ i >= 0 /\ p1 + i >= 0 /\ f1 + i >= 0 /\ -f1 + i >= 0 /\ e1 - h + 1 >= 0 /\ -k1 + h - 1 >= 0 /\ -e1 + h - 1 >= 0 /\ p1 >= 0 /\ f1 + p1 >= 0 /\ -f1 + p1 >= 0 /\ e1 - k1 >= 0 /\ -f1 >= 0 /\ f1 >= 0 /\ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(h + i + k1 + p1 + 1, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ i >= 0 /\ p1 + i >= 0 /\ f1 + i >= 0 /\ -f1 + i >= 0 /\ e1 - h + 1 >= 0 /\ -k1 + h - 1 >= 0 /\ -e1 + h - 1 >= 0 /\ p1 >= 0 /\ f1 + p1 >= 0 /\ -f1 + p1 >= 0 /\ e1 - k1 >= 0 /\ -f1 >= 0 /\ f1 >= 0 /\ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(h + i + k1 + p1 + 1, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ i >= 0 /\ p1 + i >= 0 /\ f1 + i >= 0 /\ -f1 + i >= 0 /\ e1 - h + 1 >= 0 /\ -k1 + h - 1 >= 0 /\ -e1 + h - 1 >= 0 /\ p1 >= 0 /\ f1 + p1 >= 0 /\ -f1 + p1 >= 0 /\ e1 - k1 >= 0 /\ -f1 >= 0 /\ f1 >= 0 /\ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(h + i + k1 + p1 + 1, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ i >= 0 /\ p1 + i >= 0 /\ f1 + i >= 0 /\ -f1 + i >= 0 /\ e1 - h + 1 >= 0 /\ -k1 + h - 1 >= 0 /\ -e1 + h - 1 >= 0 /\ p1 >= 0 /\ f1 + p1 >= 0 /\ -f1 + p1 >= 0 /\ e1 - k1 >= 0 /\ -f1 >= 0 /\ f1 >= 0 /\ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ y1 >= 1 /\ f1 = 0 ]
		(h + i + k1 + p1 + 1, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ i >= 0 /\ p1 + i >= 0 /\ f1 + i >= 0 /\ -f1 + i >= 0 /\ e1 - h + 1 >= 0 /\ -k1 + h - 1 >= 0 /\ -e1 + h - 1 >= 0 /\ p1 >= 0 /\ f1 + p1 >= 0 /\ -f1 + p1 >= 0 /\ e1 - k1 >= 0 /\ -f1 >= 0 /\ f1 >= 0 /\ c2 >= d1 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ y1 >= c2 + 1 /\ 0 >= y1 + 1 /\ f1 = 0 ]
		(h + i + k1 + p1 + 1, 1)    f10(a, b, c, d, h, i, l, z, d1, e1, f1, k1, p1) -> f10(a, b, c, d, h, i, y1, z, d1, e1, 0, k1 - 1, p1) [ i >= 0 /\ p1 + i >= 0 /\ f1 + i >= 0 /\ -f1 + i >= 0 /\ e1 - h + 1 >= 0 /\ -k1 + h - 1 >= 0 /\ -e1 + h - 1 >= 0 /\ p1 >= 0 /\ f1 + p1 >= 0 /\ -f1 + p1 >= 0 /\ e1 - k1 >= 0 /\ -f1 >= 0 /\ f1 >= 0 /\ d1 >= c2 + 1 /\ k1 >= 0 /\ x1 >= 2 /\ c2 >= y1 + 1 /\ y1 >= 1 /\ f1 = 0 ]
	start location:	f17
	leaf cost:	4

Complexity upper bound ?

Time: 13.311 sec (SMT: 6.252 sec)