MAYBE Initial complexity problem: 1: T: (?, 1) f12(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) -> f16(a, b, 1, l1, n1, o1, h + 1, h, p1, h, 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) [ a >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ m1 >= l1 /\ 0 >= n1 + 1 /\ c = 1 ] (?, 1) f12(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) -> f16(a, b, 1, l1, n1, o1, h + 1, h, p1, h, 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) [ a >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ m1 >= l1 /\ n1 >= 1 /\ c = 1 ] (?, 1) f12(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) -> f16(a, b, 1, l1, n1, o1, h + 1, h, p1, h, 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) [ a >= 0 /\ l1 >= 2 /\ b >= 1 /\ m1 >= l1 /\ 0 >= n1 + 1 /\ c = 1 ] (?, 1) f12(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) -> f16(a, b, 1, l1, n1, o1, h + 1, h, p1, h, 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) [ a >= 0 /\ l1 >= 2 /\ b >= 1 /\ m1 >= l1 /\ n1 >= 1 /\ c = 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) -> f16(a, b, c, l1, n1, f, g, h, i, j, o1, p1, 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) [ j >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 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) -> f16(a, b, c, l1, n1, f, g, h, i, j, o1, p1, 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) [ j >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ 0 >= n1 + 1 /\ p1 >= 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) -> f16(a, b, c, l1, n1, f, g, h, i, j, o1, p1, 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) [ j >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ n1 >= 1 /\ 0 >= p1 + 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) -> f16(a, b, c, l1, n1, f, g, h, i, j, o1, p1, 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) [ j >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ n1 >= 1 /\ p1 >= 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) -> f16(a, b, c, l1, n1, f, g, h, i, j, o1, p1, 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) [ j >= 0 /\ l1 >= 2 /\ b >= 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 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) -> f16(a, b, c, l1, n1, f, g, h, i, j, o1, p1, 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) [ j >= 0 /\ l1 >= 2 /\ b >= 1 /\ 0 >= n1 + 1 /\ p1 >= 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) -> f16(a, b, c, l1, n1, f, g, h, i, j, o1, p1, 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) [ j >= 0 /\ l1 >= 2 /\ b >= 1 /\ n1 >= 1 /\ 0 >= p1 + 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) -> f16(a, b, c, l1, n1, f, g, h, i, j, o1, p1, 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) [ j >= 0 /\ l1 >= 2 /\ b >= 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f16(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) -> f16(a, b, c + 1, l1, n1, o1, g, h - 1, i, j, k, l, b, p1, c + 1, h - 1, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f16(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) -> f16(a, b, c + 1, l1, n1, o1, g, h - 1, i, j, k, l, b, p1, c + 1, h - 1, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f16(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) -> f16(a, b, c + 1, l1, n1, o1, g, h - 1, i, j, k, l, b, p1, c + 1, h - 1, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f16(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) -> f16(a, b, c + 1, l1, n1, o1, g, h - 1, i, j, k, l, b, p1, c + 1, h - 1, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f16(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) -> f16(a, b, c + 1, l1, n1, o1, g, h - 1, i, j, k, l, b, p1, c + 1, h - 1, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f16(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) -> f16(a, b, c + 1, l1, n1, o1, g, h - 1, i, j, k, l, b, p1, c + 1, h - 1, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f16(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) -> f16(a, b, c + 1, l1, n1, o1, g, h - 1, i, j, k, l, b, p1, c + 1, h - 1, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f16(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) -> f16(a, b, c + 1, l1, n1, o1, g, h - 1, i, j, k, l, b, p1, c + 1, h - 1, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1) -> f1(a + 1, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, s, l1, s, n1, a, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1) [ q >= a + 1 /\ a >= 0 ] (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1) -> f16(h, r, 0, l1, r, f, g, h, i, j, k, l, m, n, o, p, n1, o1, r1, m1, u, v, p1, s1, t1, q1, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1) [ a >= q /\ a >= 0 /\ l1 >= 2 /\ 0 >= r + 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1) -> f16(h, r, 0, l1, r, f, g, h, i, j, k, l, m, n, o, p, n1, o1, r1, m1, u, v, p1, s1, t1, q1, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1) [ a >= q /\ a >= 0 /\ l1 >= 2 /\ r >= 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] (?, 1) f7(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) -> f8(a, 0, c, l1, n1, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, 0, n1, 0, n1, a1, h1, i1, j1, k1) [ o1 >= a1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ n1 >= o1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f7(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) -> f8(a, 0, c, l1, n1, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, 0, n1, 0, n1, a1, h1, i1, j1, k1) [ o1 >= a1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ n1 >= o1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f7(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) -> f8(a, 0, c, l1, n1, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, 0, n1, 0, n1, a1, h1, i1, j1, k1) [ o1 >= a1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ o1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f7(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) -> f8(a, 0, c, l1, n1, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, 0, n1, 0, n1, a1, h1, i1, j1, k1) [ o1 >= a1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ o1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f7(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) -> f8(a, 0, c, l1, n1, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, 0, n1, 0, n1, a1, h1, i1, j1, k1) [ a1 >= o1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ n1 >= o1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f7(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) -> f8(a, 0, c, l1, n1, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, 0, n1, 0, n1, a1, h1, i1, j1, k1) [ a1 >= o1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ n1 >= o1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f7(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) -> f8(a, 0, c, l1, n1, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, 0, n1, 0, n1, a1, h1, i1, j1, k1) [ a1 >= o1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ o1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f7(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) -> f8(a, 0, c, l1, n1, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, 0, n1, 0, n1, a1, h1, i1, j1, k1) [ a1 >= o1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ o1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f7(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) -> f10(a, b, c, l1, s1, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, t1, z, r1, b1, m1, n1, o1, p1, q1, h1, i1, j1, k1) [ b1 >= 0 /\ 0 >= s1 + 1 /\ l1 >= 2 /\ c1 = a1 ] (?, 1) f7(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) -> f10(a, b, c, l1, s1, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, t1, z, r1, b1, m1, n1, o1, p1, q1, h1, i1, j1, k1) [ b1 >= 0 /\ s1 >= 1 /\ l1 >= 2 /\ c1 = a1 ] (?, 1) f8(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) -> f8(a, 0, c, l1, n1, o1, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, 0, n1, 0, n1, a1, h1 - 1, h1 - 1, j1, k1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(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) -> f8(a, 0, c, l1, n1, o1, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, 0, n1, 0, n1, a1, h1 - 1, h1 - 1, j1, k1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(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) -> f8(a, 0, c, l1, n1, o1, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, 0, n1, 0, n1, a1, h1 - 1, h1 - 1, j1, k1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(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) -> f8(a, 0, c, l1, n1, o1, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, 0, n1, 0, n1, a1, h1 - 1, h1 - 1, j1, k1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(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) -> f8(a, 0, c, l1, n1, o1, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, 0, n1, 0, n1, a1, h1 - 1, h1 - 1, j1, k1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(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) -> f8(a, 0, c, l1, n1, o1, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, 0, n1, 0, n1, a1, h1 - 1, h1 - 1, j1, k1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(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) -> f8(a, 0, c, l1, n1, o1, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, 0, n1, 0, n1, a1, h1 - 1, h1 - 1, j1, k1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(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) -> f8(a, 0, c, l1, n1, o1, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, 0, n1, 0, n1, a1, h1 - 1, h1 - 1, j1, k1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(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) -> f10(a, b, c, l1, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, s1, z, r1, b1, m1, n1, o1, p1, t1, h1, i1, j1, k1) [ l1 >= 2 /\ h1 >= 0 /\ c1 = a1 ] (?, 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) -> f8(a, 0, h1 + 1, l1, e, f, g, h, i, 0, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, e, h1, 0, e, 0, e, e, h1, i1, j1, k1) [ n1 >= 2 /\ e >= 1 /\ l1 >= 2 /\ 0 >= e + 1 /\ b = 0 /\ j = 0 /\ c = 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) -> f8(a, 0, h1 + 1, l1, e, f, g, h, i, 0, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, e, h1, 0, e, 0, e, e, h1, i1, j1, k1) [ n1 >= 2 /\ e >= 1 /\ l1 >= 2 /\ b = 0 /\ j = 0 /\ c = 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) -> f8(a, 0, h1 + 1, l1, e, f, g, h, i, 0, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, e, h1, 0, e, 0, e, e, h1, i1, j1, k1) [ n1 >= 2 /\ 0 >= e + 1 /\ l1 >= 2 /\ b = 0 /\ j = 0 /\ c = 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) -> f8(a, 0, h1 + 1, l1, e, f, g, h, i, 0, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, e, h1, 0, e, 0, e, e, h1, i1, j1, k1) [ n1 >= 2 /\ 0 >= e + 1 /\ l1 >= 2 /\ e >= 1 /\ b = 0 /\ j = 0 /\ c = 1 ] (?, 1) f16(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) -> f8(a, 0, h1 + 1, l1, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, e, h1, 0, e, 0, e, e, h1, i1, j1, k1) [ n1 >= 2 /\ e >= 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ 0 >= e + 1 /\ b = 0 ] (?, 1) f16(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) -> f8(a, 0, h1 + 1, l1, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, e, h1, 0, e, 0, e, e, h1, i1, j1, k1) [ n1 >= 2 /\ e >= 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ b = 0 ] (?, 1) f16(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) -> f8(a, 0, h1 + 1, l1, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, e, h1, 0, e, 0, e, e, h1, i1, j1, k1) [ n1 >= 2 /\ 0 >= e + 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ b = 0 ] (?, 1) f16(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) -> f8(a, 0, h1 + 1, l1, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, e, h1, 0, e, 0, e, e, h1, i1, j1, k1) [ n1 >= 2 /\ 0 >= e + 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ e >= 1 /\ b = 0 ] (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) -> f1(2, b, c, l1, e, f, g, h, i, j, k, l, m, n, o, p, l1, o1, p1, o1, u, v, o1, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, n1, m1) [ l1 >= 2 ] (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) -> f10(s1, 0, c, l1, 0, f, g, h, i, j, k, l, m, n, o, p, q1, x1, a2, z1, u, v, y1, b2, c2, z, r1, b1, m1, n1, o1, p1, d2, h1, i1, t1, k1) [ 0 >= u1 /\ 0 >= v1 /\ 0 >= l1 /\ 0 >= w1 ] start location: f9 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c, e, h, j, q, r, s, a1, b1, c1, h1]. We thus obtain the following problem: 2: T: (1, 1) f9(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f10(s1, 0, c, 0, h, j, q1, x1, a2, r1, b1, m1, h1) [ 0 >= u1 /\ 0 >= v1 /\ 0 >= l1 /\ 0 >= w1 ] (1, 1) f9(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f1(2, b, c, e, h, j, l1, o1, p1, a1, b1, c1, h1) [ l1 >= 2 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ 0 >= e + 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ e >= 1 /\ b = 0 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ 0 >= e + 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ b = 0 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ e >= 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ b = 0 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ e >= 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ 0 >= e + 1 /\ b = 0 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, 0, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ 0 >= e + 1 /\ l1 >= 2 /\ e >= 1 /\ b = 0 /\ j = 0 /\ c = 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, 0, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ 0 >= e + 1 /\ l1 >= 2 /\ b = 0 /\ j = 0 /\ c = 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, 0, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ e >= 1 /\ l1 >= 2 /\ b = 0 /\ j = 0 /\ c = 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, 0, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ e >= 1 /\ l1 >= 2 /\ 0 >= e + 1 /\ b = 0 /\ j = 0 /\ c = 1 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f10(a, b, c, e, h, j, q, r, s, r1, b1, m1, h1) [ l1 >= 2 /\ h1 >= 0 /\ c1 = a1 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f10(a, b, c, s1, h, j, q, r, s, r1, b1, m1, h1) [ b1 >= 0 /\ s1 >= 1 /\ l1 >= 2 /\ c1 = a1 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f10(a, b, c, s1, h, j, q, r, s, r1, b1, m1, h1) [ b1 >= 0 /\ 0 >= s1 + 1 /\ l1 >= 2 /\ c1 = a1 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ a1 >= o1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ o1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ a1 >= o1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ o1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ a1 >= o1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ n1 >= o1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ a1 >= o1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ n1 >= o1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ o1 >= a1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ o1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ o1 >= a1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ o1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ o1 >= a1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ n1 >= o1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ o1 >= a1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ n1 >= o1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(h, r, 0, r, h, j, n1, o1, r1, a1, b1, c1, h1) [ a >= q /\ a >= 0 /\ l1 >= 2 /\ r >= 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] (?, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(h, r, 0, r, h, j, n1, o1, r1, a1, b1, c1, h1) [ a >= q /\ a >= 0 /\ l1 >= 2 /\ 0 >= r + 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] (?, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f1(a + 1, b, c, e, h, j, q, s, l1, a1, b1, c1, h1) [ q >= a + 1 /\ a >= 0 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ b >= 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ b >= 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ b >= 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ b >= 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f12(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, 1, n1, h, h, q, r, s, a1, b1, c1, h1) [ a >= 0 /\ l1 >= 2 /\ b >= 1 /\ m1 >= l1 /\ n1 >= 1 /\ c = 1 ] (?, 1) f12(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, 1, n1, h, h, q, r, s, a1, b1, c1, h1) [ a >= 0 /\ l1 >= 2 /\ b >= 1 /\ m1 >= l1 /\ 0 >= n1 + 1 /\ c = 1 ] (?, 1) f12(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, 1, n1, h, h, q, r, s, a1, b1, c1, h1) [ a >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ m1 >= l1 /\ n1 >= 1 /\ c = 1 ] (?, 1) f12(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, 1, n1, h, h, q, r, s, a1, b1, c1, h1) [ a >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ m1 >= l1 /\ 0 >= n1 + 1 /\ c = 1 ] start location: f9 leaf cost: 0 Testing for unsatisfiable constraints removes the following transitions from problem 2: f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ 0 >= e + 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ e >= 1 /\ b = 0 ] f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ e >= 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ 0 >= e + 1 /\ b = 0 ] f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, 0, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ 0 >= e + 1 /\ l1 >= 2 /\ e >= 1 /\ b = 0 /\ j = 0 /\ c = 1 ] f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, 0, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ e >= 1 /\ l1 >= 2 /\ 0 >= e + 1 /\ b = 0 /\ j = 0 /\ c = 1 ] We thus obtain the following problem: 3: T: (1, 1) f9(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f10(s1, 0, c, 0, h, j, q1, x1, a2, r1, b1, m1, h1) [ 0 >= u1 /\ 0 >= v1 /\ 0 >= l1 /\ 0 >= w1 ] (1, 1) f9(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f1(2, b, c, e, h, j, l1, o1, p1, a1, b1, c1, h1) [ l1 >= 2 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ 0 >= e + 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ b = 0 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ e >= 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ b = 0 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, 0, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ 0 >= e + 1 /\ l1 >= 2 /\ b = 0 /\ j = 0 /\ c = 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, 0, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ e >= 1 /\ l1 >= 2 /\ b = 0 /\ j = 0 /\ c = 1 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f10(a, b, c, e, h, j, q, r, s, r1, b1, m1, h1) [ l1 >= 2 /\ h1 >= 0 /\ c1 = a1 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f10(a, b, c, s1, h, j, q, r, s, r1, b1, m1, h1) [ b1 >= 0 /\ s1 >= 1 /\ l1 >= 2 /\ c1 = a1 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f10(a, b, c, s1, h, j, q, r, s, r1, b1, m1, h1) [ b1 >= 0 /\ 0 >= s1 + 1 /\ l1 >= 2 /\ c1 = a1 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ a1 >= o1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ o1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ a1 >= o1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ o1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ a1 >= o1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ n1 >= o1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ a1 >= o1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ n1 >= o1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ o1 >= a1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ o1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ o1 >= a1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ o1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ o1 >= a1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ n1 >= o1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ o1 >= a1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ n1 >= o1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(h, r, 0, r, h, j, n1, o1, r1, a1, b1, c1, h1) [ a >= q /\ a >= 0 /\ l1 >= 2 /\ r >= 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] (?, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(h, r, 0, r, h, j, n1, o1, r1, a1, b1, c1, h1) [ a >= q /\ a >= 0 /\ l1 >= 2 /\ 0 >= r + 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] (?, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f1(a + 1, b, c, e, h, j, q, s, l1, a1, b1, c1, h1) [ q >= a + 1 /\ a >= 0 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ b >= 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ b >= 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ b >= 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ b >= 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f12(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, 1, n1, h, h, q, r, s, a1, b1, c1, h1) [ a >= 0 /\ l1 >= 2 /\ b >= 1 /\ m1 >= l1 /\ n1 >= 1 /\ c = 1 ] (?, 1) f12(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, 1, n1, h, h, q, r, s, a1, b1, c1, h1) [ a >= 0 /\ l1 >= 2 /\ b >= 1 /\ m1 >= l1 /\ 0 >= n1 + 1 /\ c = 1 ] (?, 1) f12(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, 1, n1, h, h, q, r, s, a1, b1, c1, h1) [ a >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ m1 >= l1 /\ n1 >= 1 /\ c = 1 ] (?, 1) f12(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, 1, n1, h, h, q, r, s, a1, b1, c1, h1) [ a >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ m1 >= l1 /\ 0 >= n1 + 1 /\ c = 1 ] start location: f9 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 3 produces the following problem: 4: T: (1, 1) f9(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f1(2, b, c, e, h, j, l1, o1, p1, a1, b1, c1, h1) [ l1 >= 2 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ 0 >= e + 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ b = 0 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ e >= 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ b = 0 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, 0, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ 0 >= e + 1 /\ l1 >= 2 /\ b = 0 /\ j = 0 /\ c = 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, 0, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ e >= 1 /\ l1 >= 2 /\ b = 0 /\ j = 0 /\ c = 1 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ a1 >= o1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ o1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ a1 >= o1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ o1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ a1 >= o1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ n1 >= o1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ a1 >= o1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ n1 >= o1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ o1 >= a1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ o1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ o1 >= a1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ o1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ o1 >= a1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ n1 >= o1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ o1 >= a1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ n1 >= o1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(h, r, 0, r, h, j, n1, o1, r1, a1, b1, c1, h1) [ a >= q /\ a >= 0 /\ l1 >= 2 /\ r >= 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] (?, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(h, r, 0, r, h, j, n1, o1, r1, a1, b1, c1, h1) [ a >= q /\ a >= 0 /\ l1 >= 2 /\ 0 >= r + 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] (?, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f1(a + 1, b, c, e, h, j, q, s, l1, a1, b1, c1, h1) [ q >= a + 1 /\ a >= 0 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ b >= 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ b >= 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ b >= 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ b >= 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f12(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, 1, n1, h, h, q, r, s, a1, b1, c1, h1) [ a >= 0 /\ l1 >= 2 /\ b >= 1 /\ m1 >= l1 /\ n1 >= 1 /\ c = 1 ] (?, 1) f12(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, 1, n1, h, h, q, r, s, a1, b1, c1, h1) [ a >= 0 /\ l1 >= 2 /\ b >= 1 /\ m1 >= l1 /\ 0 >= n1 + 1 /\ c = 1 ] (?, 1) f12(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, 1, n1, h, h, q, r, s, a1, b1, c1, h1) [ a >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ m1 >= l1 /\ n1 >= 1 /\ c = 1 ] (?, 1) f12(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, 1, n1, h, h, q, r, s, a1, b1, c1, h1) [ a >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ m1 >= l1 /\ 0 >= n1 + 1 /\ c = 1 ] start location: f9 leaf cost: 4 Testing for reachability in the complexity graph removes the following transitions from problem 4: f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, 0, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ 0 >= e + 1 /\ l1 >= 2 /\ b = 0 /\ j = 0 /\ c = 1 ] f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, 0, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ e >= 1 /\ l1 >= 2 /\ b = 0 /\ j = 0 /\ c = 1 ] f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ a1 >= o1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ o1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ a1 >= o1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ o1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ a1 >= o1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ n1 >= o1 + 1 /\ n1 >= 1 /\ c1 = 0 ] f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ a1 >= o1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ n1 >= o1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ o1 >= a1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ o1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ o1 >= a1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ o1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ o1 >= a1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ n1 >= o1 + 1 /\ n1 >= 1 /\ c1 = 0 ] f7(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1) [ o1 >= a1 + 1 /\ b1 >= 0 /\ l1 >= 2 /\ n1 >= o1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ b >= 1 /\ n1 >= 1 /\ p1 >= 1 ] f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ b >= 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ b >= 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ b >= 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ n1 >= 1 /\ p1 >= 1 ] f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] f13(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c, n1, h, j, q, r, s, a1, b1, c1, h1) [ j >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] f12(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, 1, n1, h, h, q, r, s, a1, b1, c1, h1) [ a >= 0 /\ l1 >= 2 /\ b >= 1 /\ m1 >= l1 /\ n1 >= 1 /\ c = 1 ] f12(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, 1, n1, h, h, q, r, s, a1, b1, c1, h1) [ a >= 0 /\ l1 >= 2 /\ b >= 1 /\ m1 >= l1 /\ 0 >= n1 + 1 /\ c = 1 ] f12(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, 1, n1, h, h, q, r, s, a1, b1, c1, h1) [ a >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ m1 >= l1 /\ n1 >= 1 /\ c = 1 ] f12(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, 1, n1, h, h, q, r, s, a1, b1, c1, h1) [ a >= 0 /\ l1 >= 2 /\ 0 >= b + 1 /\ m1 >= l1 /\ 0 >= n1 + 1 /\ c = 1 ] We thus obtain the following problem: 5: T: (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ 0 >= e + 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ b = 0 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ e >= 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ b = 0 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f1(a + 1, b, c, e, h, j, q, s, l1, a1, b1, c1, h1) [ q >= a + 1 /\ a >= 0 ] (?, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(h, r, 0, r, h, j, n1, o1, r1, a1, b1, c1, h1) [ a >= q /\ a >= 0 /\ l1 >= 2 /\ 0 >= r + 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] (?, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(h, r, 0, r, h, j, n1, o1, r1, a1, b1, c1, h1) [ a >= q /\ a >= 0 /\ l1 >= 2 /\ r >= 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] (1, 1) f9(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f1(2, b, c, e, h, j, l1, o1, p1, a1, b1, c1, h1) [ l1 >= 2 ] start location: f9 leaf cost: 4 A polynomial rank function with Pol(f8) = -8 Pol(f16) = -5 Pol(f1) = 2 Pol(f9) = 2 orients all transitions weakly and the transitions f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(h, r, 0, r, h, j, n1, o1, r1, a1, b1, c1, h1) [ a >= q /\ a >= 0 /\ l1 >= 2 /\ r >= 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(h, r, 0, r, h, j, n1, o1, r1, a1, b1, c1, h1) [ a >= q /\ a >= 0 /\ l1 >= 2 /\ 0 >= r + 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] strictly and produces the following problem: 6: T: (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ 0 >= e + 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ b = 0 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ e >= 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ b = 0 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f1(a + 1, b, c, e, h, j, q, s, l1, a1, b1, c1, h1) [ q >= a + 1 /\ a >= 0 ] (2, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(h, r, 0, r, h, j, n1, o1, r1, a1, b1, c1, h1) [ a >= q /\ a >= 0 /\ l1 >= 2 /\ 0 >= r + 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] (2, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(h, r, 0, r, h, j, n1, o1, r1, a1, b1, c1, h1) [ a >= q /\ a >= 0 /\ l1 >= 2 /\ r >= 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] (1, 1) f9(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f1(2, b, c, e, h, j, l1, o1, p1, a1, b1, c1, h1) [ l1 >= 2 ] start location: f9 leaf cost: 4 A polynomial rank function with Pol(f8) = -8 Pol(f16) = 1 Pol(f1) = 1 Pol(f9) = 1 orients all transitions weakly and the transition f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ e >= 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ b = 0 ] strictly and produces the following problem: 7: T: (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ 0 >= e + 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ b = 0 ] (1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ e >= 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ b = 0 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f1(a + 1, b, c, e, h, j, q, s, l1, a1, b1, c1, h1) [ q >= a + 1 /\ a >= 0 ] (2, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(h, r, 0, r, h, j, n1, o1, r1, a1, b1, c1, h1) [ a >= q /\ a >= 0 /\ l1 >= 2 /\ 0 >= r + 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] (2, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(h, r, 0, r, h, j, n1, o1, r1, a1, b1, c1, h1) [ a >= q /\ a >= 0 /\ l1 >= 2 /\ r >= 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] (1, 1) f9(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f1(2, b, c, e, h, j, l1, o1, p1, a1, b1, c1, h1) [ l1 >= 2 ] start location: f9 leaf cost: 4 A polynomial rank function with Pol(f8) = -6 Pol(f16) = 1 Pol(f1) = 1 Pol(f9) = 1 orients all transitions weakly and the transition f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ 0 >= e + 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ b = 0 ] strictly and produces the following problem: 8: T: (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (?, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ 0 >= e + 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ b = 0 ] (1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ e >= 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ b = 0 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f1(a + 1, b, c, e, h, j, q, s, l1, a1, b1, c1, h1) [ q >= a + 1 /\ a >= 0 ] (2, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(h, r, 0, r, h, j, n1, o1, r1, a1, b1, c1, h1) [ a >= q /\ a >= 0 /\ l1 >= 2 /\ 0 >= r + 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] (2, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(h, r, 0, r, h, j, n1, o1, r1, a1, b1, c1, h1) [ a >= q /\ a >= 0 /\ l1 >= 2 /\ r >= 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] (1, 1) f9(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f1(2, b, c, e, h, j, l1, o1, p1, a1, b1, c1, h1) [ l1 >= 2 ] start location: f9 leaf cost: 4 A polynomial rank function with Pol(f8) = V_13 + 1 Pol(f16) = V_5 + V_13 + 1 Pol(f1) = V_3 + V_5 + V_13 + 1 Pol(f9) = V_3 + V_5 + V_13 + 1 orients all transitions weakly and the transitions f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] strictly and produces the following problem: 9: T: (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ 0 >= e + 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ b = 0 ] (1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ e >= 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ b = 0 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (?, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f1(a + 1, b, c, e, h, j, q, s, l1, a1, b1, c1, h1) [ q >= a + 1 /\ a >= 0 ] (2, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(h, r, 0, r, h, j, n1, o1, r1, a1, b1, c1, h1) [ a >= q /\ a >= 0 /\ l1 >= 2 /\ 0 >= r + 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] (2, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(h, r, 0, r, h, j, n1, o1, r1, a1, b1, c1, h1) [ a >= q /\ a >= 0 /\ l1 >= 2 /\ r >= 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] (1, 1) f9(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f1(2, b, c, e, h, j, l1, o1, p1, a1, b1, c1, h1) [ l1 >= 2 ] start location: f9 leaf cost: 4 A polynomial rank function with Pol(f8) = V_3 + V_5 - V_11 Pol(f16) = V_5 + 1 Pol(f1) = V_3 + V_5 + 1 Pol(f9) = V_3 + V_5 + 1 orients all transitions weakly and the transitions f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ p1 >= 1 ] f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ p1 >= 1 ] f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] strictly and produces the following problem: 10: T: (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ 0 >= e + 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ b = 0 ] (1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ n1 >= 2 /\ e >= 1 /\ l1 >= 2 /\ c >= 0 /\ h >= 0 /\ b = 0 ] (c + h + 1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (c + h + 1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (c + h + 1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (c + h + 1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ p1 >= 1 ] (c + h + 1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (c + h + 1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (c + h + 1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (c + h + 1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ c >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ p1 >= 1 ] (?, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f1(a + 1, b, c, e, h, j, q, s, l1, a1, b1, c1, h1) [ q >= a + 1 /\ a >= 0 ] (2, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(h, r, 0, r, h, j, n1, o1, r1, a1, b1, c1, h1) [ a >= q /\ a >= 0 /\ l1 >= 2 /\ 0 >= r + 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] (2, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(h, r, 0, r, h, j, n1, o1, r1, a1, b1, c1, h1) [ a >= q /\ a >= 0 /\ l1 >= 2 /\ r >= 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] (1, 1) f9(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f1(2, b, c, e, h, j, l1, o1, p1, a1, b1, c1, h1) [ l1 >= 2 ] start location: f9 leaf cost: 4 Applied AI with 'oct' on problem 10 to obtain the following invariants: For symbol f1: X_7 - 2 >= 0 /\ X_1 + X_7 - 4 >= 0 /\ -X_1 + X_7 >= 0 /\ X_1 - 2 >= 0 For symbol f16: X_1 - X_5 >= 0 /\ X_3 + X_5 - 2 >= 0 /\ X_3 >= 0 /\ X_1 + X_3 - 2 >= 0 /\ X_1 - 2 >= 0 For symbol f8: X_1 - X_5 >= 0 /\ X_5 >= 0 /\ X_2 + X_5 >= 0 /\ -X_2 + X_5 >= 0 /\ X_12 + X_5 >= 0 /\ -X_12 + X_5 >= 0 /\ X_1 + X_5 - 2 >= 0 /\ X_11 - X_3 + 1 >= 0 /\ -X_13 + X_3 - 1 >= 0 /\ -X_11 + X_3 - 1 >= 0 /\ -X_2 >= 0 /\ X_12 - X_2 >= 0 /\ -X_12 - X_2 >= 0 /\ X_1 - X_2 - 2 >= 0 /\ X_2 >= 0 /\ X_12 + X_2 >= 0 /\ -X_12 + X_2 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ X_11 - X_13 >= 0 /\ -X_12 >= 0 /\ X_1 - X_12 - 2 >= 0 /\ X_12 >= 0 /\ X_1 + X_12 - 2 >= 0 /\ X_1 - 2 >= 0 This yielded the following problem: 11: T: (1, 1) f9(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f1(2, b, c, e, h, j, l1, o1, p1, a1, b1, c1, h1) [ l1 >= 2 ] (2, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(h, r, 0, r, h, j, n1, o1, r1, a1, b1, c1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ a >= q /\ a >= 0 /\ l1 >= 2 /\ r >= 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] (2, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(h, r, 0, r, h, j, n1, o1, r1, a1, b1, c1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ a >= q /\ a >= 0 /\ l1 >= 2 /\ 0 >= r + 1 /\ q1 >= l1 /\ h >= l1 /\ c = 0 ] (?, 1) f1(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f1(a + 1, b, c, e, h, j, q, s, l1, a1, b1, c1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ q >= a + 1 /\ a >= 0 ] (c + h + 1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ a - h >= 0 /\ c + h - 2 >= 0 /\ c >= 0 /\ a + c - 2 >= 0 /\ a - 2 >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ p1 >= 1 ] (c + h + 1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ a - h >= 0 /\ c + h - 2 >= 0 /\ c >= 0 /\ a + c - 2 >= 0 /\ a - 2 >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (c + h + 1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ a - h >= 0 /\ c + h - 2 >= 0 /\ c >= 0 /\ a + c - 2 >= 0 /\ a - 2 >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (c + h + 1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ a - h >= 0 /\ c + h - 2 >= 0 /\ c >= 0 /\ a + c - 2 >= 0 /\ a - 2 >= 0 /\ h >= 0 /\ l1 >= 2 /\ m1 >= 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (c + h + 1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ a - h >= 0 /\ c + h - 2 >= 0 /\ c >= 0 /\ a + c - 2 >= 0 /\ a - 2 >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ p1 >= 1 ] (c + h + 1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ a - h >= 0 /\ c + h - 2 >= 0 /\ c >= 0 /\ a + c - 2 >= 0 /\ a - 2 >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ n1 >= 1 /\ 0 >= p1 + 1 ] (c + h + 1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ a - h >= 0 /\ c + h - 2 >= 0 /\ c >= 0 /\ a + c - 2 >= 0 /\ a - 2 >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ p1 >= 1 ] (c + h + 1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f16(a, b, c + 1, n1, h - 1, j, q, r, s, a1, b1, c1, h1) [ a - h >= 0 /\ c + h - 2 >= 0 /\ c >= 0 /\ a + c - 2 >= 0 /\ a - 2 >= 0 /\ h >= 0 /\ l1 >= 2 /\ 0 >= m1 + 1 /\ 0 >= n1 + 1 /\ 0 >= p1 + 1 ] (1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ a - h >= 0 /\ c + h - 2 >= 0 /\ c >= 0 /\ a + c - 2 >= 0 /\ a - 2 >= 0 /\ n1 >= 2 /\ e >= 1 /\ l1 >= 2 /\ h >= 0 /\ b = 0 ] (1, 1) f16(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, h1 + 1, e, h, j, q, r, s, e, h1, 0, h1) [ a - h >= 0 /\ c + h - 2 >= 0 /\ c >= 0 /\ a + c - 2 >= 0 /\ a - 2 >= 0 /\ n1 >= 2 /\ 0 >= e + 1 /\ l1 >= 2 /\ h >= 0 /\ b = 0 ] (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a - h >= 0 /\ h >= 0 /\ b + h >= 0 /\ -b + h >= 0 /\ c1 + h >= 0 /\ -c1 + h >= 0 /\ a + h - 2 >= 0 /\ b1 - c + 1 >= 0 /\ -h1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -b >= 0 /\ c1 - b >= 0 /\ -c1 - b >= 0 /\ a - b - 2 >= 0 /\ b >= 0 /\ c1 + b >= 0 /\ -c1 + b >= 0 /\ a + b - 2 >= 0 /\ b1 - h1 >= 0 /\ -c1 >= 0 /\ a - c1 - 2 >= 0 /\ c1 >= 0 /\ a + c1 - 2 >= 0 /\ a - 2 >= 0 /\ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a - h >= 0 /\ h >= 0 /\ b + h >= 0 /\ -b + h >= 0 /\ c1 + h >= 0 /\ -c1 + h >= 0 /\ a + h - 2 >= 0 /\ b1 - c + 1 >= 0 /\ -h1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -b >= 0 /\ c1 - b >= 0 /\ -c1 - b >= 0 /\ a - b - 2 >= 0 /\ b >= 0 /\ c1 + b >= 0 /\ -c1 + b >= 0 /\ a + b - 2 >= 0 /\ b1 - h1 >= 0 /\ -c1 >= 0 /\ a - c1 - 2 >= 0 /\ c1 >= 0 /\ a + c1 - 2 >= 0 /\ a - 2 >= 0 /\ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a - h >= 0 /\ h >= 0 /\ b + h >= 0 /\ -b + h >= 0 /\ c1 + h >= 0 /\ -c1 + h >= 0 /\ a + h - 2 >= 0 /\ b1 - c + 1 >= 0 /\ -h1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -b >= 0 /\ c1 - b >= 0 /\ -c1 - b >= 0 /\ a - b - 2 >= 0 /\ b >= 0 /\ c1 + b >= 0 /\ -c1 + b >= 0 /\ a + b - 2 >= 0 /\ b1 - h1 >= 0 /\ -c1 >= 0 /\ a - c1 - 2 >= 0 /\ c1 >= 0 /\ a + c1 - 2 >= 0 /\ a - 2 >= 0 /\ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a - h >= 0 /\ h >= 0 /\ b + h >= 0 /\ -b + h >= 0 /\ c1 + h >= 0 /\ -c1 + h >= 0 /\ a + h - 2 >= 0 /\ b1 - c + 1 >= 0 /\ -h1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -b >= 0 /\ c1 - b >= 0 /\ -c1 - b >= 0 /\ a - b - 2 >= 0 /\ b >= 0 /\ c1 + b >= 0 /\ -c1 + b >= 0 /\ a + b - 2 >= 0 /\ b1 - h1 >= 0 /\ -c1 >= 0 /\ a - c1 - 2 >= 0 /\ c1 >= 0 /\ a + c1 - 2 >= 0 /\ a - 2 >= 0 /\ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a - h >= 0 /\ h >= 0 /\ b + h >= 0 /\ -b + h >= 0 /\ c1 + h >= 0 /\ -c1 + h >= 0 /\ a + h - 2 >= 0 /\ b1 - c + 1 >= 0 /\ -h1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -b >= 0 /\ c1 - b >= 0 /\ -c1 - b >= 0 /\ a - b - 2 >= 0 /\ b >= 0 /\ c1 + b >= 0 /\ -c1 + b >= 0 /\ a + b - 2 >= 0 /\ b1 - h1 >= 0 /\ -c1 >= 0 /\ a - c1 - 2 >= 0 /\ c1 >= 0 /\ a + c1 - 2 >= 0 /\ a - 2 >= 0 /\ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a - h >= 0 /\ h >= 0 /\ b + h >= 0 /\ -b + h >= 0 /\ c1 + h >= 0 /\ -c1 + h >= 0 /\ a + h - 2 >= 0 /\ b1 - c + 1 >= 0 /\ -h1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -b >= 0 /\ c1 - b >= 0 /\ -c1 - b >= 0 /\ a - b - 2 >= 0 /\ b >= 0 /\ c1 + b >= 0 /\ -c1 + b >= 0 /\ a + b - 2 >= 0 /\ b1 - h1 >= 0 /\ -c1 >= 0 /\ a - c1 - 2 >= 0 /\ c1 >= 0 /\ a + c1 - 2 >= 0 /\ a - 2 >= 0 /\ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ n1 >= 1 /\ c1 = 0 ] (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a - h >= 0 /\ h >= 0 /\ b + h >= 0 /\ -b + h >= 0 /\ c1 + h >= 0 /\ -c1 + h >= 0 /\ a + h - 2 >= 0 /\ b1 - c + 1 >= 0 /\ -h1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -b >= 0 /\ c1 - b >= 0 /\ -c1 - b >= 0 /\ a - b - 2 >= 0 /\ b >= 0 /\ c1 + b >= 0 /\ -c1 + b >= 0 /\ a + b - 2 >= 0 /\ b1 - h1 >= 0 /\ -c1 >= 0 /\ a - c1 - 2 >= 0 /\ c1 >= 0 /\ a + c1 - 2 >= 0 /\ a - 2 >= 0 /\ p1 >= a1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ n1 >= p1 + 1 /\ 0 >= n1 + 1 /\ c1 = 0 ] (c + h + h1 + 1, 1) f8(a, b, c, e, h, j, q, r, s, a1, b1, c1, h1) -> f8(a, 0, c, n1, h, j, q, r, s, a1, b1, 0, h1 - 1) [ a - h >= 0 /\ h >= 0 /\ b + h >= 0 /\ -b + h >= 0 /\ c1 + h >= 0 /\ -c1 + h >= 0 /\ a + h - 2 >= 0 /\ b1 - c + 1 >= 0 /\ -h1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -b >= 0 /\ c1 - b >= 0 /\ -c1 - b >= 0 /\ a - b - 2 >= 0 /\ b >= 0 /\ c1 + b >= 0 /\ -c1 + b >= 0 /\ a + b - 2 >= 0 /\ b1 - h1 >= 0 /\ -c1 >= 0 /\ a - c1 - 2 >= 0 /\ c1 >= 0 /\ a + c1 - 2 >= 0 /\ a - 2 >= 0 /\ a1 >= p1 + 1 /\ h1 >= 0 /\ l1 >= 2 /\ p1 >= n1 + 1 /\ n1 >= 1 /\ c1 = 0 ] start location: f9 leaf cost: 4 Complexity upper bound ? Time: 10.663 sec (SMT: 6.224 sec)