MAYBE Initial complexity problem: 1: T: (?, 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, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) -> f14(e, c2, e2, d, e, 0, d, a2, d2, f2, g2, h2, i2, j2, c, c, d, c, t, t, b2, k2, 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, x1, y1, z1) [ a >= b /\ a >= 0 /\ c >= d + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 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, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) -> f14(e, c2, e2, d, e, 0, d, a2, d2, f2, g2, h2, i2, j2, c, c, d, c, t, t, b2, k2, 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, x1, y1, z1) [ a >= b /\ a >= 0 /\ d >= c + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 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, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) -> f7(a + 1, b, n, d, e, f, g, h, i, j, k, l, n, a2, o, p, q, r, s, t, u, v, c2, a, t, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ b >= a + 1 /\ a >= 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, x1, y1, z1) -> f14(a, b, c, q, e, 1, q, a2, i, j, k, l, m, n, c2, c2, q, r, s, t, u, v, w, x, y, d2, e + 1, t, e2, f2, e, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ g2 >= r + 1 /\ a >= 0 /\ a2 >= 2 /\ c2 >= g2 + 1 /\ h2 >= a2 /\ f = 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, x1, y1, z1) -> f14(a, b, c, q, e, 1, q, a2, i, j, k, l, m, n, c2, c2, q, r, s, t, u, v, w, x, y, d2, e + 1, t, e2, f2, e, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ g2 >= r + 1 /\ a >= 0 /\ a2 >= 2 /\ g2 >= c2 + 1 /\ h2 >= a2 /\ f = 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, x1, y1, z1) -> f14(a, b, c, q, e, 1, q, a2, i, j, k, l, m, n, c2, c2, q, r, s, t, u, v, w, x, y, d2, e + 1, t, e2, f2, e, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ r >= g2 + 1 /\ a >= 0 /\ a2 >= 2 /\ c2 >= g2 + 1 /\ h2 >= a2 /\ f = 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, x1, y1, z1) -> f14(a, b, c, q, e, 1, q, a2, i, j, k, l, m, n, c2, c2, q, r, s, t, u, v, w, x, y, d2, e + 1, t, e2, f2, e, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ r >= g2 + 1 /\ a >= 0 /\ a2 >= 2 /\ g2 >= c2 + 1 /\ h2 >= a2 /\ f = 1 ] (?, 1) f10(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) -> f14(a, b, c, q, e, f, q, a2, i, j, k, l, m, n, c2, c2, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, d2, e2, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ f2 >= r + 1 /\ f2 >= e2 + 1 /\ e1 >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 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, x1, y1, z1) -> f14(a, b, c, q, e, f, q, a2, i, j, k, l, m, n, c2, c2, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, d2, e2, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ f2 >= r + 1 /\ f2 >= e2 + 1 /\ e1 >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 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, x1, y1, z1) -> f14(a, b, c, q, e, f, q, a2, i, j, k, l, m, n, c2, c2, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, d2, e2, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ f2 >= r + 1 /\ e2 >= f2 + 1 /\ e1 >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 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, x1, y1, z1) -> f14(a, b, c, q, e, f, q, a2, i, j, k, l, m, n, c2, c2, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, d2, e2, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ f2 >= r + 1 /\ e2 >= f2 + 1 /\ e1 >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 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, x1, y1, z1) -> f14(a, b, c, q, e, f, q, a2, i, j, k, l, m, n, c2, c2, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, d2, e2, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ r >= f2 + 1 /\ f2 >= e2 + 1 /\ e1 >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 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, x1, y1, z1) -> f14(a, b, c, q, e, f, q, a2, i, j, k, l, m, n, c2, c2, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, d2, e2, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ r >= f2 + 1 /\ f2 >= e2 + 1 /\ e1 >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 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, x1, y1, z1) -> f14(a, b, c, q, e, f, q, a2, i, j, k, l, m, n, c2, c2, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, d2, e2, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ r >= f2 + 1 /\ e2 >= f2 + 1 /\ e1 >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 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, x1, y1, z1) -> f14(a, b, c, q, e, f, q, a2, i, j, k, l, m, n, c2, c2, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, d2, e2, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ r >= f2 + 1 /\ e2 >= f2 + 1 /\ e1 >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(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, x1, y1, z1) -> f14(a, b, c, q, e - 1, f + 1, q, a2, i, j, k, l, m, n, c2, c2, q, r, s, t, u, v, w, x, y, d2, a1, b1, c1, d1, e1, f1, g1, r, e2, t, f + 1, e - 1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(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, x1, y1, z1) -> f14(a, b, c, q, e - 1, f + 1, q, a2, i, j, k, l, m, n, c2, c2, q, r, s, t, u, v, w, x, y, d2, a1, b1, c1, d1, e1, f1, g1, r, e2, t, f + 1, e - 1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(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, x1, y1, z1) -> f14(a, b, c, q, e - 1, f + 1, q, a2, i, j, k, l, m, n, c2, c2, q, r, s, t, u, v, w, x, y, d2, a1, b1, c1, d1, e1, f1, g1, r, e2, t, f + 1, e - 1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(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, x1, y1, z1) -> f14(a, b, c, q, e - 1, f + 1, q, a2, i, j, k, l, m, n, c2, c2, q, r, s, t, u, v, w, x, y, d2, a1, b1, c1, d1, e1, f1, g1, r, e2, t, f + 1, e - 1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(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, x1, y1, z1) -> f14(a, b, c, q, e - 1, f + 1, q, a2, i, j, k, l, m, n, c2, c2, q, r, s, t, u, v, w, x, y, d2, a1, b1, c1, d1, e1, f1, g1, r, e2, t, f + 1, e - 1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(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, x1, y1, z1) -> f14(a, b, c, q, e - 1, f + 1, q, a2, i, j, k, l, m, n, c2, c2, q, r, s, t, u, v, w, x, y, d2, a1, b1, c1, d1, e1, f1, g1, r, e2, t, f + 1, e - 1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(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, x1, y1, z1) -> f14(a, b, c, q, e - 1, f + 1, q, a2, i, j, k, l, m, n, c2, c2, q, r, s, t, u, v, w, x, y, d2, a1, b1, c1, d1, e1, f1, g1, r, e2, t, f + 1, e - 1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(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, x1, y1, z1) -> f14(a, b, c, q, e - 1, f + 1, q, a2, i, j, k, l, m, n, c2, c2, q, r, s, t, u, v, w, x, y, d2, a1, b1, c1, d1, e1, f1, g1, r, e2, t, f + 1, e - 1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f4(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, x1, y1, z1) -> f5(a, b, c, o1, e, f, o1, a2, i, j, k, l, m, n, c2, 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, c2, m1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ d2 >= m1 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= d2 + 1 ] (?, 1) f4(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, x1, y1, z1) -> f5(a, b, c, o1, e, f, o1, a2, i, j, k, l, m, n, c2, 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, c2, m1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ d2 >= m1 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ d2 >= c2 + 1 ] (?, 1) f4(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, x1, y1, z1) -> f5(a, b, c, o1, e, f, o1, a2, i, j, k, l, m, n, c2, 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, c2, m1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ d2 >= m1 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= d2 + 1 ] (?, 1) f4(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, x1, y1, z1) -> f5(a, b, c, o1, e, f, o1, a2, i, j, k, l, m, n, c2, 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, c2, m1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ d2 >= m1 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ d2 >= c2 + 1 ] (?, 1) f4(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, x1, y1, z1) -> f5(a, b, c, o1, e, f, o1, a2, i, j, k, l, m, n, c2, 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, c2, m1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ m1 >= d2 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= d2 + 1 ] (?, 1) f4(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, x1, y1, z1) -> f5(a, b, c, o1, e, f, o1, a2, i, j, k, l, m, n, c2, 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, c2, m1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ m1 >= d2 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ d2 >= c2 + 1 ] (?, 1) f4(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, x1, y1, z1) -> f5(a, b, c, o1, e, f, o1, a2, i, j, k, l, m, n, c2, 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, c2, m1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ m1 >= d2 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= d2 + 1 ] (?, 1) f4(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, x1, y1, z1) -> f5(a, b, c, o1, e, f, o1, a2, i, j, k, l, m, n, c2, 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, c2, m1, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ m1 >= d2 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ d2 >= c2 + 1 ] (?, 1) f4(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, x1, y1, z1) -> f16(a, b, c, d, e, f, a2, c2, i, j, d2, l, m, n, e2, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, h2, n1, g2, f2, i2, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ n1 >= 0 /\ a2 >= e2 + 1 /\ c2 >= 2 /\ o1 = m1 ] (?, 1) f4(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, x1, y1, z1) -> f16(a, b, c, d, e, f, a2, c2, i, j, d2, l, m, n, e2, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, h2, n1, g2, f2, i2, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ n1 >= 0 /\ e2 >= a2 + 1 /\ c2 >= 2 /\ o1 = m1 ] (?, 1) f5(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, x1, y1, z1) -> f5(a, b, c, o1, e, f, o1, a2, i, j, k, l, m, n, c2, p, q, r, s, t, u, v, w, x, y, d2, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, c2, m1, r1 - 1, t, r1 - 1, u1, v1, w1, x1, y1, z1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(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, x1, y1, z1) -> f5(a, b, c, o1, e, f, o1, a2, i, j, k, l, m, n, c2, p, q, r, s, t, u, v, w, x, y, d2, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, c2, m1, r1 - 1, t, r1 - 1, u1, v1, w1, x1, y1, z1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(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, x1, y1, z1) -> f5(a, b, c, o1, e, f, o1, a2, i, j, k, l, m, n, c2, p, q, r, s, t, u, v, w, x, y, d2, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, c2, m1, r1 - 1, t, r1 - 1, u1, v1, w1, x1, y1, z1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(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, x1, y1, z1) -> f5(a, b, c, o1, e, f, o1, a2, i, j, k, l, m, n, c2, p, q, r, s, t, u, v, w, x, y, d2, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, c2, m1, r1 - 1, t, r1 - 1, u1, v1, w1, x1, y1, z1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(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, x1, y1, z1) -> f5(a, b, c, o1, e, f, o1, a2, i, j, k, l, m, n, c2, p, q, r, s, t, u, v, w, x, y, d2, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, c2, m1, r1 - 1, t, r1 - 1, u1, v1, w1, x1, y1, z1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(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, x1, y1, z1) -> f5(a, b, c, o1, e, f, o1, a2, i, j, k, l, m, n, c2, p, q, r, s, t, u, v, w, x, y, d2, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, c2, m1, r1 - 1, t, r1 - 1, u1, v1, w1, x1, y1, z1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(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, x1, y1, z1) -> f5(a, b, c, o1, e, f, o1, a2, i, j, k, l, m, n, c2, p, q, r, s, t, u, v, w, x, y, d2, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, c2, m1, r1 - 1, t, r1 - 1, u1, v1, w1, x1, y1, z1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(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, x1, y1, z1) -> f5(a, b, c, o1, e, f, o1, a2, i, j, k, l, m, n, c2, p, q, r, s, t, u, v, w, x, y, d2, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, c2, m1, r1 - 1, t, r1 - 1, u1, v1, w1, x1, y1, z1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(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, x1, y1, z1) -> f16(a, b, c, d, e, f, g, a2, i, j, c2, 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, f2, n1, e2, d2, g2, r1, s1, t1, u1, v1, w1, x1, y1, z1) [ a2 >= 2 /\ r1 >= 0 /\ o1 = m1 ] (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, x1, y1, z1) -> f7(2, e2, f2, a2, e, f, a2, e2, a2, j, k, f2, f2, g2, 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, c2, d2, h2, x1, y1, z1) [ e2 >= 2 ] (?, 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, x1, y1, z1) -> f5(a, b, c, d, e, r1 + 1, d, a2, i, j, k, l, m, n, o, c2, d2, e2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, o, r1, d, o, o, r1, s1, t1, u1, v1, w1, t, t, f2) [ g2 >= 2 /\ a2 >= 2 /\ e1 >= 0 /\ o >= d + 1 /\ d >= o + 1 /\ q = r /\ f = 1 ] (?, 1) f10(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) -> f5(a, b, c, d, e, r1 + 1, d, a2, i, j, k, l, m, n, o, c2, d2, e2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, o, r1, d, o, o, r1, s1, t1, u1, v1, w1, t, t, f2) [ g2 >= 2 /\ a2 >= 2 /\ e1 >= 0 /\ o >= d + 1 /\ q = r /\ f = 1 ] (?, 1) f10(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) -> f5(a, b, c, d, e, r1 + 1, d, a2, i, j, k, l, m, n, o, c2, d2, e2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, o, r1, d, o, o, r1, s1, t1, u1, v1, w1, t, t, f2) [ g2 >= 2 /\ a2 >= 2 /\ e1 >= 0 /\ d >= o + 1 /\ q = r /\ f = 1 ] (?, 1) f10(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1) -> f5(a, b, c, d, e, r1 + 1, d, a2, i, j, k, l, m, n, o, c2, d2, e2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, o, r1, d, o, o, r1, s1, t1, u1, v1, w1, t, t, f2) [ g2 >= 2 /\ a2 >= 2 /\ e1 >= 0 /\ d >= o + 1 /\ o >= d + 1 /\ q = r /\ f = 1 ] (?, 1) f14(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, x1, y1, z1) -> f5(a, b, c, d, e, r1 + 1, d, a2, i, j, k, l, m, n, o, c2, d2, e2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, o, r1, d, o, o, r1, s1, t1, u1, v1, w1, x1, t, f2) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ o >= d + 1 /\ d >= o + 1 /\ q = r ] (?, 1) f14(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, x1, y1, z1) -> f5(a, b, c, d, e, r1 + 1, d, a2, i, j, k, l, m, n, o, c2, d2, e2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, o, r1, d, o, o, r1, s1, t1, u1, v1, w1, x1, t, f2) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ o >= d + 1 /\ q = r ] (?, 1) f14(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, x1, y1, z1) -> f5(a, b, c, d, e, r1 + 1, d, a2, i, j, k, l, m, n, o, c2, d2, e2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, o, r1, d, o, o, r1, s1, t1, u1, v1, w1, x1, t, f2) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ d >= o + 1 /\ q = r ] (?, 1) f14(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, x1, y1, z1) -> f5(a, b, c, d, e, r1 + 1, d, a2, i, j, k, l, m, n, o, c2, d2, e2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, o, r1, d, o, o, r1, s1, t1, u1, v1, w1, x1, t, f2) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ d >= o + 1 /\ o >= d + 1 /\ q = r ] (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, x1, y1, z1) -> f16(h2, e2, g2, u1, e, f, u1, d2, f2, i2, j2, b2, k2, o2, u1, p2, q2, r2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, u2, n1, t2, s2, v2, r1, s1, t1, a2, c2, w1, x1, y1, z1) [ 0 >= l2 /\ 0 >= m2 /\ 0 >= d2 /\ 0 >= n2 ] (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, x1, y1, z1) -> f16(h2, e2, g2, n, e, f, a2, 1, f2, i2, j2, b2, k2, o2, p2, q2, r2, s2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, v2, n1, u2, t2, l2, r1, s1, t1, c2, d2, w1, x1, y1, z1) [ 0 >= 1 /\ a2 >= p2 + 1 ] (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, x1, y1, z1) -> f16(h2, e2, g2, n, e, f, a2, 1, f2, i2, j2, b2, k2, o2, p2, q2, r2, s2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, v2, n1, u2, t2, l2, r1, s1, t1, c2, d2, w1, x1, y1, z1) [ 0 >= 1 /\ p2 >= a2 + 1 ] (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, x1, y1, z1) -> f16(h2, e2, g2, n, e, f, a2, 1, f2, i2, j2, b2, k2, o2, p2, q2, r2, s2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, v2, n1, u2, t2, l2, r1, s1, t1, c2, d2, w1, x1, y1, z1) [ 0 >= 1 /\ a2 >= p2 + 1 ] (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, x1, y1, z1) -> f16(h2, e2, g2, n, e, f, a2, 1, f2, i2, j2, b2, k2, o2, p2, q2, r2, s2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, v2, n1, u2, t2, l2, r1, s1, t1, c2, d2, w1, x1, y1, z1) [ 0 >= 1 /\ p2 >= a2 + 1 ] start location: f15 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1]. We thus obtain the following problem: 2: T: (1, 1) f15(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f16(h2, e2, g2, n, e, f, o2, p2, r2, s2, e1, v2, n1, u2, r1, c2) [ 0 >= 1 /\ p2 >= a2 + 1 ] (1, 1) f15(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f16(h2, e2, g2, n, e, f, o2, p2, r2, s2, e1, v2, n1, u2, r1, c2) [ 0 >= 1 /\ a2 >= p2 + 1 ] (1, 1) f15(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f16(h2, e2, g2, n, e, f, o2, p2, r2, s2, e1, v2, n1, u2, r1, c2) [ 0 >= 1 /\ p2 >= a2 + 1 ] (1, 1) f15(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f16(h2, e2, g2, n, e, f, o2, p2, r2, s2, e1, v2, n1, u2, r1, c2) [ 0 >= 1 /\ a2 >= p2 + 1 ] (1, 1) f15(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f16(h2, e2, g2, u1, e, f, o2, u1, q2, r2, e1, u2, n1, t2, r1, a2) [ 0 >= l2 /\ 0 >= m2 /\ 0 >= d2 /\ 0 >= n2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ d >= o + 1 /\ o >= d + 1 /\ q = r ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ d >= o + 1 /\ q = r ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ o >= d + 1 /\ q = r ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ o >= d + 1 /\ d >= o + 1 /\ q = r ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e1 >= 0 /\ d >= o + 1 /\ o >= d + 1 /\ q = r /\ f = 1 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e1 >= 0 /\ d >= o + 1 /\ q = r /\ f = 1 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e1 >= 0 /\ o >= d + 1 /\ q = r /\ f = 1 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e1 >= 0 /\ o >= d + 1 /\ d >= o + 1 /\ q = r /\ f = 1 ] (1, 1) f15(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f7(2, e2, f2, a2, e, f, g2, o, q, r, e1, m1, n1, o1, r1, c2) [ e2 >= 2 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f16(a, b, c, d, e, f, n, o, q, r, e1, f2, n1, e2, r1, u1) [ a2 >= 2 /\ r1 >= 0 /\ o1 = m1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f16(a, b, c, d, e, f, n, e2, q, r, e1, h2, n1, g2, r1, u1) [ n1 >= 0 /\ e2 >= a2 + 1 /\ c2 >= 2 /\ o1 = m1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f16(a, b, c, d, e, f, n, e2, q, r, e1, h2, n1, g2, r1, u1) [ n1 >= 0 /\ a2 >= e2 + 1 /\ c2 >= 2 /\ o1 = m1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ m1 >= d2 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ d2 >= c2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ m1 >= d2 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= d2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ m1 >= d2 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ d2 >= c2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ m1 >= d2 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= d2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d2 >= m1 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ d2 >= c2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d2 >= m1 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= d2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d2 >= m1 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ d2 >= c2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d2 >= m1 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= d2 + 1 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ r >= f2 + 1 /\ e2 >= f2 + 1 /\ e1 >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ r >= f2 + 1 /\ e2 >= f2 + 1 /\ e1 >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ r >= f2 + 1 /\ f2 >= e2 + 1 /\ e1 >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ r >= f2 + 1 /\ f2 >= e2 + 1 /\ e1 >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= r + 1 /\ e2 >= f2 + 1 /\ e1 >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= r + 1 /\ e2 >= f2 + 1 /\ e1 >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= r + 1 /\ f2 >= e2 + 1 /\ e1 >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= r + 1 /\ f2 >= e2 + 1 /\ e1 >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f9(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, 1, n, c2, q, r, e, m1, n1, o1, r1, u1) [ r >= g2 + 1 /\ a >= 0 /\ a2 >= 2 /\ g2 >= c2 + 1 /\ h2 >= a2 /\ f = 1 ] (?, 1) f9(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, 1, n, c2, q, r, e, m1, n1, o1, r1, u1) [ r >= g2 + 1 /\ a >= 0 /\ a2 >= 2 /\ c2 >= g2 + 1 /\ h2 >= a2 /\ f = 1 ] (?, 1) f9(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, 1, n, c2, q, r, e, m1, n1, o1, r1, u1) [ g2 >= r + 1 /\ a >= 0 /\ a2 >= 2 /\ g2 >= c2 + 1 /\ h2 >= a2 /\ f = 1 ] (?, 1) f9(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, 1, n, c2, q, r, e, m1, n1, o1, r1, u1) [ g2 >= r + 1 /\ a >= 0 /\ a2 >= 2 /\ c2 >= g2 + 1 /\ h2 >= a2 /\ f = 1 ] (?, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f7(a + 1, b, n, d, e, f, a2, o, q, r, e1, m1, n1, o1, r1, u1) [ b >= a + 1 /\ a >= 0 ] (?, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(e, c2, e2, d, e, 0, j2, c, d, c, e1, m1, n1, o1, r1, u1) [ a >= b /\ a >= 0 /\ d >= c + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 0 ] (?, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(e, c2, e2, d, e, 0, j2, c, d, c, e1, m1, n1, o1, r1, u1) [ a >= b /\ a >= 0 /\ c >= d + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 0 ] start location: f15 leaf cost: 0 Testing for unsatisfiable constraints removes the following transitions from problem 2: f15(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f16(h2, e2, g2, n, e, f, o2, p2, r2, s2, e1, v2, n1, u2, r1, c2) [ 0 >= 1 /\ p2 >= a2 + 1 ] f15(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f16(h2, e2, g2, n, e, f, o2, p2, r2, s2, e1, v2, n1, u2, r1, c2) [ 0 >= 1 /\ a2 >= p2 + 1 ] f15(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f16(h2, e2, g2, n, e, f, o2, p2, r2, s2, e1, v2, n1, u2, r1, c2) [ 0 >= 1 /\ p2 >= a2 + 1 ] f15(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f16(h2, e2, g2, n, e, f, o2, p2, r2, s2, e1, v2, n1, u2, r1, c2) [ 0 >= 1 /\ a2 >= p2 + 1 ] f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ d >= o + 1 /\ o >= d + 1 /\ q = r ] f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ o >= d + 1 /\ d >= o + 1 /\ q = r ] f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e1 >= 0 /\ d >= o + 1 /\ o >= d + 1 /\ q = r /\ f = 1 ] f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e1 >= 0 /\ o >= d + 1 /\ d >= o + 1 /\ q = r /\ f = 1 ] We thus obtain the following problem: 3: T: (1, 1) f15(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f16(h2, e2, g2, u1, e, f, o2, u1, q2, r2, e1, u2, n1, t2, r1, a2) [ 0 >= l2 /\ 0 >= m2 /\ 0 >= d2 /\ 0 >= n2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ d >= o + 1 /\ q = r ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ o >= d + 1 /\ q = r ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e1 >= 0 /\ d >= o + 1 /\ q = r /\ f = 1 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e1 >= 0 /\ o >= d + 1 /\ q = r /\ f = 1 ] (1, 1) f15(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f7(2, e2, f2, a2, e, f, g2, o, q, r, e1, m1, n1, o1, r1, c2) [ e2 >= 2 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f16(a, b, c, d, e, f, n, o, q, r, e1, f2, n1, e2, r1, u1) [ a2 >= 2 /\ r1 >= 0 /\ o1 = m1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f16(a, b, c, d, e, f, n, e2, q, r, e1, h2, n1, g2, r1, u1) [ n1 >= 0 /\ e2 >= a2 + 1 /\ c2 >= 2 /\ o1 = m1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f16(a, b, c, d, e, f, n, e2, q, r, e1, h2, n1, g2, r1, u1) [ n1 >= 0 /\ a2 >= e2 + 1 /\ c2 >= 2 /\ o1 = m1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ m1 >= d2 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ d2 >= c2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ m1 >= d2 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= d2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ m1 >= d2 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ d2 >= c2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ m1 >= d2 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= d2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d2 >= m1 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ d2 >= c2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d2 >= m1 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= d2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d2 >= m1 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ d2 >= c2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d2 >= m1 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= d2 + 1 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ r >= f2 + 1 /\ e2 >= f2 + 1 /\ e1 >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ r >= f2 + 1 /\ e2 >= f2 + 1 /\ e1 >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ r >= f2 + 1 /\ f2 >= e2 + 1 /\ e1 >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ r >= f2 + 1 /\ f2 >= e2 + 1 /\ e1 >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= r + 1 /\ e2 >= f2 + 1 /\ e1 >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= r + 1 /\ e2 >= f2 + 1 /\ e1 >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= r + 1 /\ f2 >= e2 + 1 /\ e1 >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= r + 1 /\ f2 >= e2 + 1 /\ e1 >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f9(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, 1, n, c2, q, r, e, m1, n1, o1, r1, u1) [ r >= g2 + 1 /\ a >= 0 /\ a2 >= 2 /\ g2 >= c2 + 1 /\ h2 >= a2 /\ f = 1 ] (?, 1) f9(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, 1, n, c2, q, r, e, m1, n1, o1, r1, u1) [ r >= g2 + 1 /\ a >= 0 /\ a2 >= 2 /\ c2 >= g2 + 1 /\ h2 >= a2 /\ f = 1 ] (?, 1) f9(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, 1, n, c2, q, r, e, m1, n1, o1, r1, u1) [ g2 >= r + 1 /\ a >= 0 /\ a2 >= 2 /\ g2 >= c2 + 1 /\ h2 >= a2 /\ f = 1 ] (?, 1) f9(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, 1, n, c2, q, r, e, m1, n1, o1, r1, u1) [ g2 >= r + 1 /\ a >= 0 /\ a2 >= 2 /\ c2 >= g2 + 1 /\ h2 >= a2 /\ f = 1 ] (?, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f7(a + 1, b, n, d, e, f, a2, o, q, r, e1, m1, n1, o1, r1, u1) [ b >= a + 1 /\ a >= 0 ] (?, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(e, c2, e2, d, e, 0, j2, c, d, c, e1, m1, n1, o1, r1, u1) [ a >= b /\ a >= 0 /\ d >= c + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 0 ] (?, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(e, c2, e2, d, e, 0, j2, c, d, c, e1, m1, n1, o1, r1, u1) [ a >= b /\ a >= 0 /\ c >= d + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 0 ] start location: f15 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 3 produces the following problem: 4: T: (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ d >= o + 1 /\ q = r ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ o >= d + 1 /\ q = r ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e1 >= 0 /\ d >= o + 1 /\ q = r /\ f = 1 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e1 >= 0 /\ o >= d + 1 /\ q = r /\ f = 1 ] (1, 1) f15(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f7(2, e2, f2, a2, e, f, g2, o, q, r, e1, m1, n1, o1, r1, c2) [ e2 >= 2 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ m1 >= d2 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ d2 >= c2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ m1 >= d2 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= d2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ m1 >= d2 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ d2 >= c2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ m1 >= d2 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= d2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d2 >= m1 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ d2 >= c2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d2 >= m1 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= d2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d2 >= m1 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ d2 >= c2 + 1 ] (?, 1) f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d2 >= m1 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= d2 + 1 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ r >= f2 + 1 /\ e2 >= f2 + 1 /\ e1 >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ r >= f2 + 1 /\ e2 >= f2 + 1 /\ e1 >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ r >= f2 + 1 /\ f2 >= e2 + 1 /\ e1 >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ r >= f2 + 1 /\ f2 >= e2 + 1 /\ e1 >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= r + 1 /\ e2 >= f2 + 1 /\ e1 >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= r + 1 /\ e2 >= f2 + 1 /\ e1 >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= r + 1 /\ f2 >= e2 + 1 /\ e1 >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= r + 1 /\ f2 >= e2 + 1 /\ e1 >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f9(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, 1, n, c2, q, r, e, m1, n1, o1, r1, u1) [ r >= g2 + 1 /\ a >= 0 /\ a2 >= 2 /\ g2 >= c2 + 1 /\ h2 >= a2 /\ f = 1 ] (?, 1) f9(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, 1, n, c2, q, r, e, m1, n1, o1, r1, u1) [ r >= g2 + 1 /\ a >= 0 /\ a2 >= 2 /\ c2 >= g2 + 1 /\ h2 >= a2 /\ f = 1 ] (?, 1) f9(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, 1, n, c2, q, r, e, m1, n1, o1, r1, u1) [ g2 >= r + 1 /\ a >= 0 /\ a2 >= 2 /\ g2 >= c2 + 1 /\ h2 >= a2 /\ f = 1 ] (?, 1) f9(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, 1, n, c2, q, r, e, m1, n1, o1, r1, u1) [ g2 >= r + 1 /\ a >= 0 /\ a2 >= 2 /\ c2 >= g2 + 1 /\ h2 >= a2 /\ f = 1 ] (?, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f7(a + 1, b, n, d, e, f, a2, o, q, r, e1, m1, n1, o1, r1, u1) [ b >= a + 1 /\ a >= 0 ] (?, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(e, c2, e2, d, e, 0, j2, c, d, c, e1, m1, n1, o1, r1, u1) [ a >= b /\ a >= 0 /\ d >= c + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 0 ] (?, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(e, c2, e2, d, e, 0, j2, c, d, c, e1, m1, n1, o1, r1, u1) [ a >= b /\ a >= 0 /\ c >= d + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 0 ] start location: f15 leaf cost: 4 Testing for reachability in the complexity graph removes the following transitions from problem 4: f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e1 >= 0 /\ d >= o + 1 /\ q = r /\ f = 1 ] f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e1 >= 0 /\ o >= d + 1 /\ q = r /\ f = 1 ] f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ m1 >= d2 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ d2 >= c2 + 1 ] f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ m1 >= d2 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= d2 + 1 ] f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ m1 >= d2 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ d2 >= c2 + 1 ] f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ m1 >= d2 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= d2 + 1 ] f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d2 >= m1 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ d2 >= c2 + 1 ] f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d2 >= m1 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= d2 + 1 ] f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d2 >= m1 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ d2 >= c2 + 1 ] f4(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d2 >= m1 + 1 /\ n1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= d2 + 1 ] f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ r >= f2 + 1 /\ e2 >= f2 + 1 /\ e1 >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ r >= f2 + 1 /\ e2 >= f2 + 1 /\ e1 >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ r >= f2 + 1 /\ f2 >= e2 + 1 /\ e1 >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ r >= f2 + 1 /\ f2 >= e2 + 1 /\ e1 >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= r + 1 /\ e2 >= f2 + 1 /\ e1 >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= r + 1 /\ e2 >= f2 + 1 /\ e1 >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= r + 1 /\ f2 >= e2 + 1 /\ e1 >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] f10(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, f, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= r + 1 /\ f2 >= e2 + 1 /\ e1 >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] f9(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, 1, n, c2, q, r, e, m1, n1, o1, r1, u1) [ r >= g2 + 1 /\ a >= 0 /\ a2 >= 2 /\ g2 >= c2 + 1 /\ h2 >= a2 /\ f = 1 ] f9(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, 1, n, c2, q, r, e, m1, n1, o1, r1, u1) [ r >= g2 + 1 /\ a >= 0 /\ a2 >= 2 /\ c2 >= g2 + 1 /\ h2 >= a2 /\ f = 1 ] f9(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, 1, n, c2, q, r, e, m1, n1, o1, r1, u1) [ g2 >= r + 1 /\ a >= 0 /\ a2 >= 2 /\ g2 >= c2 + 1 /\ h2 >= a2 /\ f = 1 ] f9(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e, 1, n, c2, q, r, e, m1, n1, o1, r1, u1) [ g2 >= r + 1 /\ a >= 0 /\ a2 >= 2 /\ c2 >= g2 + 1 /\ h2 >= a2 /\ f = 1 ] We thus obtain the following problem: 5: T: (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ o >= d + 1 /\ q = r ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ d >= o + 1 /\ q = r ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(e, c2, e2, d, e, 0, j2, c, d, c, e1, m1, n1, o1, r1, u1) [ a >= b /\ a >= 0 /\ c >= d + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 0 ] (?, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(e, c2, e2, d, e, 0, j2, c, d, c, e1, m1, n1, o1, r1, u1) [ a >= b /\ a >= 0 /\ d >= c + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 0 ] (?, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f7(a + 1, b, n, d, e, f, a2, o, q, r, e1, m1, n1, o1, r1, u1) [ b >= a + 1 /\ a >= 0 ] (1, 1) f15(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f7(2, e2, f2, a2, e, f, g2, o, q, r, e1, m1, n1, o1, r1, c2) [ e2 >= 2 ] start location: f15 leaf cost: 4 A polynomial rank function with Pol(f5) = -8 Pol(f14) = 1 Pol(f7) = 2 Pol(f15) = 2 orients all transitions weakly and the transitions f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(e, c2, e2, d, e, 0, j2, c, d, c, e1, m1, n1, o1, r1, u1) [ a >= b /\ a >= 0 /\ c >= d + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 0 ] f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ d >= o + 1 /\ q = r ] strictly and produces the following problem: 6: T: (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ o >= d + 1 /\ q = r ] (2, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ d >= o + 1 /\ q = r ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (2, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(e, c2, e2, d, e, 0, j2, c, d, c, e1, m1, n1, o1, r1, u1) [ a >= b /\ a >= 0 /\ c >= d + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 0 ] (?, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(e, c2, e2, d, e, 0, j2, c, d, c, e1, m1, n1, o1, r1, u1) [ a >= b /\ a >= 0 /\ d >= c + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 0 ] (?, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f7(a + 1, b, n, d, e, f, a2, o, q, r, e1, m1, n1, o1, r1, u1) [ b >= a + 1 /\ a >= 0 ] (1, 1) f15(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f7(2, e2, f2, a2, e, f, g2, o, q, r, e1, m1, n1, o1, r1, c2) [ e2 >= 2 ] start location: f15 leaf cost: 4 A polynomial rank function with Pol(f5) = -8 Pol(f14) = -7 Pol(f7) = 1 Pol(f15) = 1 orients all transitions weakly and the transition f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(e, c2, e2, d, e, 0, j2, c, d, c, e1, m1, n1, o1, r1, u1) [ a >= b /\ a >= 0 /\ d >= c + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 0 ] strictly and produces the following problem: 7: T: (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ o >= d + 1 /\ q = r ] (2, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ d >= o + 1 /\ q = r ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (2, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(e, c2, e2, d, e, 0, j2, c, d, c, e1, m1, n1, o1, r1, u1) [ a >= b /\ a >= 0 /\ c >= d + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 0 ] (1, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(e, c2, e2, d, e, 0, j2, c, d, c, e1, m1, n1, o1, r1, u1) [ a >= b /\ a >= 0 /\ d >= c + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 0 ] (?, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f7(a + 1, b, n, d, e, f, a2, o, q, r, e1, m1, n1, o1, r1, u1) [ b >= a + 1 /\ a >= 0 ] (1, 1) f15(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f7(2, e2, f2, a2, e, f, g2, o, q, r, e1, m1, n1, o1, r1, c2) [ e2 >= 2 ] start location: f15 leaf cost: 4 A polynomial rank function with Pol(f5) = -8 Pol(f14) = 1 Pol(f7) = 1 Pol(f15) = 1 orients all transitions weakly and the transition f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ o >= d + 1 /\ q = r ] strictly and produces the following problem: 8: T: (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] (?, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] (1, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ o >= d + 1 /\ q = r ] (2, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ d >= o + 1 /\ q = r ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (2, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(e, c2, e2, d, e, 0, j2, c, d, c, e1, m1, n1, o1, r1, u1) [ a >= b /\ a >= 0 /\ c >= d + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 0 ] (1, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(e, c2, e2, d, e, 0, j2, c, d, c, e1, m1, n1, o1, r1, u1) [ a >= b /\ a >= 0 /\ d >= c + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 0 ] (?, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f7(a + 1, b, n, d, e, f, a2, o, q, r, e1, m1, n1, o1, r1, u1) [ b >= a + 1 /\ a >= 0 ] (1, 1) f15(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f7(2, e2, f2, a2, e, f, g2, o, q, r, e1, m1, n1, o1, r1, c2) [ e2 >= 2 ] start location: f15 leaf cost: 4 A polynomial rank function with Pol(f5) = V_15 + 1 Pol(f14) = V_5 + V_15 + 1 Pol(f7) = V_5 - V_6 + V_15 + 1 Pol(f15) = V_5 - V_6 + V_15 + 1 orients all transitions weakly and the transitions f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] strictly and produces the following problem: 9: T: (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] (1, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ o >= d + 1 /\ q = r ] (2, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ d >= o + 1 /\ q = r ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (?, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (2, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(e, c2, e2, d, e, 0, j2, c, d, c, e1, m1, n1, o1, r1, u1) [ a >= b /\ a >= 0 /\ c >= d + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 0 ] (1, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(e, c2, e2, d, e, 0, j2, c, d, c, e1, m1, n1, o1, r1, u1) [ a >= b /\ a >= 0 /\ d >= c + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 0 ] (?, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f7(a + 1, b, n, d, e, f, a2, o, q, r, e1, m1, n1, o1, r1, u1) [ b >= a + 1 /\ a >= 0 ] (1, 1) f15(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f7(2, e2, f2, a2, e, f, g2, o, q, r, e1, m1, n1, o1, r1, c2) [ e2 >= 2 ] start location: f15 leaf cost: 4 A polynomial rank function with Pol(f5) = V_5 + V_6 - V_13 Pol(f14) = V_5 + 1 Pol(f7) = V_5 + V_6 + 1 Pol(f15) = V_5 + V_6 + 1 orients all transitions weakly and the transitions f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] strictly and produces the following problem: 10: T: (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] (1, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ o >= d + 1 /\ q = r ] (2, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ f >= 0 /\ d >= o + 1 /\ q = r ] (e + f + 1, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (e + f + 1, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (e + f + 1, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (e + f + 1, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (e + f + 1, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (e + f + 1, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (e + f + 1, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (e + f + 1, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ f >= 0 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (2, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(e, c2, e2, d, e, 0, j2, c, d, c, e1, m1, n1, o1, r1, u1) [ a >= b /\ a >= 0 /\ c >= d + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 0 ] (1, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(e, c2, e2, d, e, 0, j2, c, d, c, e1, m1, n1, o1, r1, u1) [ a >= b /\ a >= 0 /\ d >= c + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 0 ] (?, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f7(a + 1, b, n, d, e, f, a2, o, q, r, e1, m1, n1, o1, r1, u1) [ b >= a + 1 /\ a >= 0 ] (1, 1) f15(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f7(2, e2, f2, a2, e, f, g2, o, q, r, e1, m1, n1, o1, r1, c2) [ e2 >= 2 ] start location: f15 leaf cost: 4 Applied AI with 'oct' on problem 10 to obtain the following invariants: For symbol f14: X_4 - X_9 >= 0 /\ -X_4 + X_9 >= 0 /\ X_6 >= 0 /\ X_5 + X_6 - 2 >= 0 /\ X_1 + X_6 - 2 >= 0 /\ X_1 - X_5 >= 0 /\ X_1 - 2 >= 0 For symbol f5: X_13 - X_6 + 1 >= 0 /\ -X_15 + X_6 - 1 >= 0 /\ -X_13 + X_6 - 1 >= 0 /\ X_1 - X_5 >= 0 /\ X_5 >= 0 /\ X_1 + X_5 - 2 >= 0 /\ X_14 - X_4 >= 0 /\ -X_14 + X_4 >= 0 /\ X_13 - X_15 >= 0 /\ X_1 - 2 >= 0 For symbol f7: X_2 - 2 >= 0 /\ X_1 + X_2 - 4 >= 0 /\ -X_1 + X_2 >= 0 /\ X_1 - 2 >= 0 This yielded the following problem: 11: T: (1, 1) f15(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f7(2, e2, f2, a2, e, f, g2, o, q, r, e1, m1, n1, o1, r1, c2) [ e2 >= 2 ] (?, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f7(a + 1, b, n, d, e, f, a2, o, q, r, e1, m1, n1, o1, r1, u1) [ b - 2 >= 0 /\ a + b - 4 >= 0 /\ -a + b >= 0 /\ a - 2 >= 0 /\ b >= a + 1 /\ a >= 0 ] (1, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(e, c2, e2, d, e, 0, j2, c, d, c, e1, m1, n1, o1, r1, u1) [ b - 2 >= 0 /\ a + b - 4 >= 0 /\ -a + b >= 0 /\ a - 2 >= 0 /\ a >= b /\ a >= 0 /\ d >= c + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 0 ] (2, 1) f7(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(e, c2, e2, d, e, 0, j2, c, d, c, e1, m1, n1, o1, r1, u1) [ b - 2 >= 0 /\ a + b - 4 >= 0 /\ -a + b >= 0 /\ a - 2 >= 0 /\ a >= b /\ a >= 0 /\ c >= d + 1 /\ a2 >= 2 /\ b2 >= a2 /\ e >= a2 /\ f = 0 ] (e + f + 1, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d - q >= 0 /\ -d + q >= 0 /\ f >= 0 /\ e + f - 2 >= 0 /\ a + f - 2 >= 0 /\ a - e >= 0 /\ a - 2 >= 0 /\ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (e + f + 1, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d - q >= 0 /\ -d + q >= 0 /\ f >= 0 /\ e + f - 2 >= 0 /\ a + f - 2 >= 0 /\ a - e >= 0 /\ a - 2 >= 0 /\ g2 >= f2 + 1 /\ e2 >= f2 + 1 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (e + f + 1, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d - q >= 0 /\ -d + q >= 0 /\ f >= 0 /\ e + f - 2 >= 0 /\ a + f - 2 >= 0 /\ a - e >= 0 /\ a - 2 >= 0 /\ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (e + f + 1, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d - q >= 0 /\ -d + q >= 0 /\ f >= 0 /\ e + f - 2 >= 0 /\ a + f - 2 >= 0 /\ a - e >= 0 /\ a - 2 >= 0 /\ g2 >= f2 + 1 /\ f2 >= e2 + 1 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (e + f + 1, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d - q >= 0 /\ -d + q >= 0 /\ f >= 0 /\ e + f - 2 >= 0 /\ a + f - 2 >= 0 /\ a - e >= 0 /\ a - 2 >= 0 /\ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (e + f + 1, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d - q >= 0 /\ -d + q >= 0 /\ f >= 0 /\ e + f - 2 >= 0 /\ a + f - 2 >= 0 /\ a - e >= 0 /\ a - 2 >= 0 /\ f2 >= g2 + 1 /\ e2 >= f2 + 1 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (e + f + 1, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d - q >= 0 /\ -d + q >= 0 /\ f >= 0 /\ e + f - 2 >= 0 /\ a + f - 2 >= 0 /\ a - e >= 0 /\ a - 2 >= 0 /\ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ e >= 0 /\ f2 >= c2 + 1 /\ a2 >= 2 ] (e + f + 1, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f14(a, b, c, q, e - 1, f + 1, n, c2, q, r, e1, m1, n1, o1, r1, u1) [ d - q >= 0 /\ -d + q >= 0 /\ f >= 0 /\ e + f - 2 >= 0 /\ a + f - 2 >= 0 /\ a - e >= 0 /\ a - 2 >= 0 /\ f2 >= g2 + 1 /\ f2 >= e2 + 1 /\ e >= 0 /\ c2 >= f2 + 1 /\ a2 >= 2 ] (2, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ d - q >= 0 /\ -d + q >= 0 /\ f >= 0 /\ e + f - 2 >= 0 /\ a + f - 2 >= 0 /\ a - e >= 0 /\ a - 2 >= 0 /\ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ d >= o + 1 /\ q = r ] (1, 1) f14(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, d, e, r1 + 1, n, o, d2, e2, e1, o, r1, d, r1, u1) [ d - q >= 0 /\ -d + q >= 0 /\ f >= 0 /\ e + f - 2 >= 0 /\ a + f - 2 >= 0 /\ a - e >= 0 /\ a - 2 >= 0 /\ g2 >= 2 /\ a2 >= 2 /\ e >= 0 /\ o >= d + 1 /\ q = r ] (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ n1 - f + 1 >= 0 /\ -r1 + f - 1 >= 0 /\ -n1 + f - 1 >= 0 /\ a - e >= 0 /\ e >= 0 /\ a + e - 2 >= 0 /\ o1 - d >= 0 /\ -o1 + d >= 0 /\ n1 - r1 >= 0 /\ a - 2 >= 0 /\ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ n1 - f + 1 >= 0 /\ -r1 + f - 1 >= 0 /\ -n1 + f - 1 >= 0 /\ a - e >= 0 /\ e >= 0 /\ a + e - 2 >= 0 /\ o1 - d >= 0 /\ -o1 + d >= 0 /\ n1 - r1 >= 0 /\ a - 2 >= 0 /\ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ n1 - f + 1 >= 0 /\ -r1 + f - 1 >= 0 /\ -n1 + f - 1 >= 0 /\ a - e >= 0 /\ e >= 0 /\ a + e - 2 >= 0 /\ o1 - d >= 0 /\ -o1 + d >= 0 /\ n1 - r1 >= 0 /\ a - 2 >= 0 /\ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ n1 - f + 1 >= 0 /\ -r1 + f - 1 >= 0 /\ -n1 + f - 1 >= 0 /\ a - e >= 0 /\ e >= 0 /\ a + e - 2 >= 0 /\ o1 - d >= 0 /\ -o1 + d >= 0 /\ n1 - r1 >= 0 /\ a - 2 >= 0 /\ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ n1 - f + 1 >= 0 /\ -r1 + f - 1 >= 0 /\ -n1 + f - 1 >= 0 /\ a - e >= 0 /\ e >= 0 /\ a + e - 2 >= 0 /\ o1 - d >= 0 /\ -o1 + d >= 0 /\ n1 - r1 >= 0 /\ a - 2 >= 0 /\ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ c2 >= e2 + 1 ] (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ n1 - f + 1 >= 0 /\ -r1 + f - 1 >= 0 /\ -n1 + f - 1 >= 0 /\ a - e >= 0 /\ e >= 0 /\ a + e - 2 >= 0 /\ o1 - d >= 0 /\ -o1 + d >= 0 /\ n1 - r1 >= 0 /\ a - 2 >= 0 /\ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ e2 >= c2 + 1 ] (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ n1 - f + 1 >= 0 /\ -r1 + f - 1 >= 0 /\ -n1 + f - 1 >= 0 /\ a - e >= 0 /\ e >= 0 /\ a + e - 2 >= 0 /\ o1 - d >= 0 /\ -o1 + d >= 0 /\ n1 - r1 >= 0 /\ a - 2 >= 0 /\ e2 >= m1 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ o1 >= c2 + 1 /\ c2 >= e2 + 1 ] (e + f + r1 + 1, 1) f5(a, b, c, d, e, f, n, o, q, r, e1, m1, n1, o1, r1, u1) -> f5(a, b, c, o1, e, f, n, c2, q, r, e1, m1, n1, o1, r1 - 1, u1) [ n1 - f + 1 >= 0 /\ -r1 + f - 1 >= 0 /\ -n1 + f - 1 >= 0 /\ a - e >= 0 /\ e >= 0 /\ a + e - 2 >= 0 /\ o1 - d >= 0 /\ -o1 + d >= 0 /\ n1 - r1 >= 0 /\ a - 2 >= 0 /\ m1 >= e2 + 1 /\ r1 >= 0 /\ a2 >= 2 /\ c2 >= o1 + 1 /\ e2 >= c2 + 1 ] start location: f15 leaf cost: 4 Complexity upper bound ? Time: 14.148 sec (SMT: 7.136 sec)