MAYBE Initial complexity problem: 1: T: (?, 1) f12(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1) -> f116(a, b, 1, -1, f, f, z1, f + 1, a2, z1, 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) [ a >= 2 /\ y1 >= a /\ b >= 0 /\ c = 1 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1) -> f116(a, b, 2, d, z1, z1 - 1, g, h, i, a2, 2, -1, y1, b2, 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) [ e >= 0 /\ a >= 2 ] (?, 1) f116(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) -> f300(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, 1, 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) [ f >= o /\ p = 1 ] (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1) -> f1(a, b + 1, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, s, z1, s, 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) [ b >= 0 /\ q >= b + 1 ] (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1) -> f116(a, z1, 0, d, e, f, g, h, i, j, k, l, m, n, o, p, a2, y1, d2, b2, r, r, e2, f2, g2, z1, c2, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1) [ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 ] (?, 1) f7(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1) -> f8(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, z1, d1, d1, z1 - 1, -1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1) [ b1 >= 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) -> 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, e2, z, a1, b1, f2, d2, e1, f1, b2, z1, a2, y1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1) [ b1 >= 0 /\ g1 = d1 ] (?, 1) f8(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1) -> f8(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, 0, h1, w, x, y, z, a1, b1, d1, d1, e1 - 1, f1, 0, h1, 0, h1, e1 - 1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1) [ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] (?, 1) f8(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1) -> f10(e2, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, f2, z, a1, b1, g2, d2, e1, f1, b2, z1, a2, y1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1) [ e1 >= 0 /\ g1 = d1 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1) -> f8(a, b, e1 + 1, d, 0, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, 0, v, w, x, y, z, a1, e1, v, v, e1, f1, 0, v, 0, v, k1, -1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1) [ a >= 2 /\ u = 0 /\ e = 0 /\ c = 1 ] (?, 1) f116(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) -> f116(a, b, c + 1, d, e, f - 1, g, h, i, j, k, l, m, n, f, 1, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, u, c + 1, f - 1, p1, q1, r1, s1, t1, u1, v1, w1, x1) [ a >= 2 /\ c >= 0 /\ f >= 0 /\ p = 0 /\ u = m1 ] (?, 1) f116(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) -> f8(a, b, e1 + 1, d, e, f, g, h, i, j, k, l, m, n, f, 1, q, r, s, t, 0, v, w, x, y, z, a1, e1, v, v, e1, f1, 0, v, 0, v, k1, -1, m1, n1, o1, z1, q1, r1, s1, t1, u1, v1, w1, x1) [ z1 >= 0 /\ a >= 2 /\ c >= 0 /\ f >= 0 /\ u = 0 /\ p = 0 ] (1, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1) -> f1(z1, 2, c, d, e, f, g, h, i, j, k, l, m, n, o, 0, z1, s, b2, s, u, v, s, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, a2, y1, d2, 2, e2, v1, w1, x1) [ z1 >= 2 /\ s = w ] (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) -> f10(f2, e2, c, d, e, f, g, h, i, j, k, l, m, n, o, 0, c2, h2, j2, i2, 0, 0, k2, l2, m2, z, a1, b1, n2, d2, e1, f1, b2, z1, a2, y1, k1, l1, m1, n1, o1, p1, q1, g2, s1, t1, u1, v1, w1, x1) [ 0 >= f2 ] (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) -> f10(1, e2, c, d, e, f, g, h, i, j, k, l, m, n, o, 0, h2, i2, k2, j2, 0, 0, m2, n2, o2, z, a1, b1, q2, d2, e1, f1, b2, z1, a2, y1, k1, l1, m1, n1, o1, p1, g2, c2, l2, t1, u1, f2, g2, p2) [ s = 0 /\ w = 0 ] start location: f9 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1]. We thus obtain the following problem: 2: T: (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f10(1, e2, c, e, f, o, 0, h2, i2, k2, 0, 0, m2, b1, d2, e1, b2, z1, a2, y1, m1) [ s = 0 /\ w = 0 ] (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f10(f2, e2, c, e, f, o, 0, c2, h2, j2, 0, 0, k2, b1, d2, e1, b2, z1, a2, y1, m1) [ 0 >= f2 ] (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(z1, 2, c, e, f, o, 0, z1, s, b2, u, v, s, b1, d1, e1, g1, h1, i1, j1, m1) [ z1 >= 2 /\ s = w ] (?, 1) f116(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, e1 + 1, e, f, f, 1, q, r, s, 0, v, w, e1, v, e1, 0, v, 0, v, m1) [ z1 >= 0 /\ a >= 2 /\ c >= 0 /\ f >= 0 /\ u = 0 /\ p = 0 ] (?, 1) f116(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f116(a, b, c + 1, e, f - 1, f, 1, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, u) [ a >= 2 /\ c >= 0 /\ f >= 0 /\ p = 0 /\ u = m1 ] (?, 1) f13(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, e1 + 1, 0, f, o, p, q, r, s, 0, v, w, e1, v, e1, 0, v, 0, v, m1) [ a >= 2 /\ u = 0 /\ e = 0 /\ c = 1 ] (?, 1) f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f10(e2, b, c, e, f, o, p, q, r, s, u, v, w, b1, d2, e1, b2, z1, a2, y1, m1) [ e1 >= 0 /\ g1 = d1 ] (?, 1) f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, 0, h1, w, b1, d1, e1 - 1, 0, h1, 0, h1, m1) [ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] (?, 1) f7(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f10(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d2, e1, b2, z1, a2, y1, m1) [ b1 >= 0 /\ g1 = d1 ] (?, 1) f7(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, u, v, w, z1, d1, z1 - 1, g1, h1, i1, j1, m1) [ b1 >= 0 ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f116(a, z1, 0, e, f, o, p, a2, y1, d2, r, r, e2, b1, d1, e1, g1, h1, i1, j1, m1) [ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(a, b + 1, c, e, f, o, p, q, s, z1, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ b >= 0 /\ q >= b + 1 ] (?, 1) f116(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f300(a, b, c, e, f, o, 1, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ f >= o /\ p = 1 ] (?, 1) f13(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f116(a, b, 2, z1, z1 - 1, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ e >= 0 /\ a >= 2 ] (?, 1) f12(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f116(a, b, 1, f, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ a >= 2 /\ y1 >= a /\ b >= 0 /\ c = 1 ] start location: f9 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(z1, 2, c, e, f, o, 0, z1, s, b2, u, v, s, b1, d1, e1, g1, h1, i1, j1, m1) [ z1 >= 2 /\ s = w ] (?, 1) f116(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, e1 + 1, e, f, f, 1, q, r, s, 0, v, w, e1, v, e1, 0, v, 0, v, m1) [ z1 >= 0 /\ a >= 2 /\ c >= 0 /\ f >= 0 /\ u = 0 /\ p = 0 ] (?, 1) f13(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, e1 + 1, 0, f, o, p, q, r, s, 0, v, w, e1, v, e1, 0, v, 0, v, m1) [ a >= 2 /\ u = 0 /\ e = 0 /\ c = 1 ] (?, 1) f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, 0, h1, w, b1, d1, e1 - 1, 0, h1, 0, h1, m1) [ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] (?, 1) f7(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, u, v, w, z1, d1, z1 - 1, g1, h1, i1, j1, m1) [ b1 >= 0 ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f116(a, z1, 0, e, f, o, p, a2, y1, d2, r, r, e2, b1, d1, e1, g1, h1, i1, j1, m1) [ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(a, b + 1, c, e, f, o, p, q, s, z1, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ b >= 0 /\ q >= b + 1 ] (?, 1) f13(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f116(a, b, 2, z1, z1 - 1, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ e >= 0 /\ a >= 2 ] (?, 1) f12(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f116(a, b, 1, f, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ a >= 2 /\ y1 >= a /\ b >= 0 /\ c = 1 ] start location: f9 leaf cost: 6 Testing for reachability in the complexity graph removes the following transitions from problem 3: f13(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, e1 + 1, 0, f, o, p, q, r, s, 0, v, w, e1, v, e1, 0, v, 0, v, m1) [ a >= 2 /\ u = 0 /\ e = 0 /\ c = 1 ] f7(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, u, v, w, z1, d1, z1 - 1, g1, h1, i1, j1, m1) [ b1 >= 0 ] f13(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f116(a, b, 2, z1, z1 - 1, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ e >= 0 /\ a >= 2 ] f12(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f116(a, b, 1, f, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ a >= 2 /\ y1 >= a /\ b >= 0 /\ c = 1 ] We thus obtain the following problem: 4: T: (?, 1) f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, 0, h1, w, b1, d1, e1 - 1, 0, h1, 0, h1, m1) [ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] (?, 1) f116(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, e1 + 1, e, f, f, 1, q, r, s, 0, v, w, e1, v, e1, 0, v, 0, v, m1) [ z1 >= 0 /\ a >= 2 /\ c >= 0 /\ f >= 0 /\ u = 0 /\ p = 0 ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(a, b + 1, c, e, f, o, p, q, s, z1, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ b >= 0 /\ q >= b + 1 ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f116(a, z1, 0, e, f, o, p, a2, y1, d2, r, r, e2, b1, d1, e1, g1, h1, i1, j1, m1) [ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 ] (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(z1, 2, c, e, f, o, 0, z1, s, b2, u, v, s, b1, d1, e1, g1, h1, i1, j1, m1) [ z1 >= 2 /\ s = w ] start location: f9 leaf cost: 6 A polynomial rank function with Pol(f8) = -2 Pol(f116) = 1 Pol(f1) = 2 Pol(f9) = 2 orients all transitions weakly and the transitions f116(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, e1 + 1, e, f, f, 1, q, r, s, 0, v, w, e1, v, e1, 0, v, 0, v, m1) [ z1 >= 0 /\ a >= 2 /\ c >= 0 /\ f >= 0 /\ u = 0 /\ p = 0 ] f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f116(a, z1, 0, e, f, o, p, a2, y1, d2, r, r, e2, b1, d1, e1, g1, h1, i1, j1, m1) [ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 ] strictly and produces the following problem: 5: T: (?, 1) f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, 0, h1, w, b1, d1, e1 - 1, 0, h1, 0, h1, m1) [ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] (2, 1) f116(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, e1 + 1, e, f, f, 1, q, r, s, 0, v, w, e1, v, e1, 0, v, 0, v, m1) [ z1 >= 0 /\ a >= 2 /\ c >= 0 /\ f >= 0 /\ u = 0 /\ p = 0 ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(a, b + 1, c, e, f, o, p, q, s, z1, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ b >= 0 /\ q >= b + 1 ] (2, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f116(a, z1, 0, e, f, o, p, a2, y1, d2, r, r, e2, b1, d1, e1, g1, h1, i1, j1, m1) [ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 ] (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(z1, 2, c, e, f, o, 0, z1, s, b2, u, v, s, b1, d1, e1, g1, h1, i1, j1, m1) [ z1 >= 2 /\ s = w ] start location: f9 leaf cost: 6 A polynomial rank function with Pol(f8) = V_16 + 1 Pol(f116) = V_7 + V_16 + 1 Pol(f1) = -V_1 + V_3 + V_5 + V_7 + V_16 + 1 Pol(f9) = V_3 + V_5 + V_16 - 1 orients all transitions weakly and the transition f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, 0, h1, w, b1, d1, e1 - 1, 0, h1, 0, h1, m1) [ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] strictly and produces the following problem: 6: T: (c + f + e1 + 1, 1) f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, 0, h1, w, b1, d1, e1 - 1, 0, h1, 0, h1, m1) [ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] (2, 1) f116(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, e1 + 1, e, f, f, 1, q, r, s, 0, v, w, e1, v, e1, 0, v, 0, v, m1) [ z1 >= 0 /\ a >= 2 /\ c >= 0 /\ f >= 0 /\ u = 0 /\ p = 0 ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(a, b + 1, c, e, f, o, p, q, s, z1, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ b >= 0 /\ q >= b + 1 ] (2, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f116(a, z1, 0, e, f, o, p, a2, y1, d2, r, r, e2, b1, d1, e1, g1, h1, i1, j1, m1) [ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 ] (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(z1, 2, c, e, f, o, 0, z1, s, b2, u, v, s, b1, d1, e1, g1, h1, i1, j1, m1) [ z1 >= 2 /\ s = w ] start location: f9 leaf cost: 6 Applied AI with 'oct' on problem 6 to obtain the following invariants: For symbol f1: X_8 - 2 >= 0 /\ X_7 + X_8 - 2 >= 0 /\ -X_7 + X_8 - 2 >= 0 /\ X_2 + X_8 - 4 >= 0 /\ -X_2 + X_8 >= 0 /\ -X_7 >= 0 /\ X_2 - X_7 - 2 >= 0 /\ X_7 >= 0 /\ X_2 + X_7 - 2 >= 0 /\ X_2 - 2 >= 0 For symbol f116: -X_7 >= 0 /\ X_5 - X_7 - 2 >= 0 /\ X_3 - X_7 >= 0 /\ -X_3 - X_7 >= 0 /\ X_1 - X_7 - 2 >= 0 /\ X_7 >= 0 /\ X_5 + X_7 - 2 >= 0 /\ X_3 + X_7 >= 0 /\ -X_3 + X_7 >= 0 /\ X_1 + X_7 - 2 >= 0 /\ X_5 - 2 >= 0 /\ X_3 + X_5 - 2 >= 0 /\ -X_3 + X_5 - 2 >= 0 /\ X_1 + X_5 - 4 >= 0 /\ -X_1 + X_5 >= 0 /\ -X_3 >= 0 /\ X_1 - X_3 - 2 >= 0 /\ X_3 >= 0 /\ X_1 + X_3 - 2 >= 0 /\ X_11 - X_12 >= 0 /\ -X_11 + X_12 >= 0 /\ X_1 - 2 >= 0 For symbol f8: -X_7 + 1 >= 0 /\ X_6 - X_7 - 1 >= 0 /\ X_5 - X_7 - 1 >= 0 /\ X_20 - X_7 + 1 >= 0 /\ -X_20 - X_7 + 1 >= 0 /\ X_19 - X_7 + 1 >= 0 /\ -X_19 - X_7 + 1 >= 0 /\ X_18 - X_7 + 1 >= 0 /\ -X_18 - X_7 + 1 >= 0 /\ X_17 - X_7 + 1 >= 0 /\ -X_17 - X_7 + 1 >= 0 /\ X_15 - X_7 + 1 >= 0 /\ -X_15 - X_7 + 1 >= 0 /\ X_12 - X_7 + 1 >= 0 /\ -X_12 - X_7 + 1 >= 0 /\ X_11 - X_7 + 1 >= 0 /\ -X_11 - X_7 + 1 >= 0 /\ X_1 - X_7 - 1 >= 0 /\ X_7 - 1 >= 0 /\ X_6 + X_7 - 3 >= 0 /\ X_5 + X_7 - 3 >= 0 /\ X_20 + X_7 - 1 >= 0 /\ -X_20 + X_7 - 1 >= 0 /\ X_19 + X_7 - 1 >= 0 /\ -X_19 + X_7 - 1 >= 0 /\ X_18 + X_7 - 1 >= 0 /\ -X_18 + X_7 - 1 >= 0 /\ X_17 + X_7 - 1 >= 0 /\ -X_17 + X_7 - 1 >= 0 /\ X_15 + X_7 - 1 >= 0 /\ -X_15 + X_7 - 1 >= 0 /\ X_12 + X_7 - 1 >= 0 /\ -X_12 + X_7 - 1 >= 0 /\ X_11 + X_7 - 1 >= 0 /\ -X_11 + X_7 - 1 >= 0 /\ X_1 + X_7 - 3 >= 0 /\ X_5 - X_6 >= 0 /\ X_6 - 2 >= 0 /\ X_5 + X_6 - 4 >= 0 /\ -X_5 + X_6 >= 0 /\ X_20 + X_6 - 2 >= 0 /\ -X_20 + X_6 - 2 >= 0 /\ X_19 + X_6 - 2 >= 0 /\ -X_19 + X_6 - 2 >= 0 /\ X_18 + X_6 - 2 >= 0 /\ -X_18 + X_6 - 2 >= 0 /\ X_17 + X_6 - 2 >= 0 /\ -X_17 + X_6 - 2 >= 0 /\ X_15 + X_6 - 2 >= 0 /\ -X_15 + X_6 - 2 >= 0 /\ X_12 + X_6 - 2 >= 0 /\ -X_12 + X_6 - 2 >= 0 /\ X_11 + X_6 - 2 >= 0 /\ -X_11 + X_6 - 2 >= 0 /\ X_1 + X_6 - 4 >= 0 /\ -X_1 + X_6 >= 0 /\ X_5 - 2 >= 0 /\ X_20 + X_5 - 2 >= 0 /\ -X_20 + X_5 - 2 >= 0 /\ X_19 + X_5 - 2 >= 0 /\ -X_19 + X_5 - 2 >= 0 /\ X_18 + X_5 - 2 >= 0 /\ -X_18 + X_5 - 2 >= 0 /\ X_17 + X_5 - 2 >= 0 /\ -X_17 + X_5 - 2 >= 0 /\ X_15 + X_5 - 2 >= 0 /\ -X_15 + X_5 - 2 >= 0 /\ X_12 + X_5 - 2 >= 0 /\ -X_12 + X_5 - 2 >= 0 /\ X_11 + X_5 - 2 >= 0 /\ -X_11 + X_5 - 2 >= 0 /\ X_1 + X_5 - 4 >= 0 /\ -X_1 + X_5 >= 0 /\ X_14 - X_3 + 1 >= 0 /\ -X_16 + X_3 - 1 >= 0 /\ -X_14 + X_3 - 1 >= 0 /\ -X_20 >= 0 /\ X_19 - X_20 >= 0 /\ -X_19 - X_20 >= 0 /\ X_18 - X_20 >= 0 /\ -X_18 - X_20 >= 0 /\ X_17 - X_20 >= 0 /\ -X_17 - X_20 >= 0 /\ X_15 - X_20 >= 0 /\ -X_15 - X_20 >= 0 /\ X_12 - X_20 >= 0 /\ -X_12 - X_20 >= 0 /\ X_11 - X_20 >= 0 /\ -X_11 - X_20 >= 0 /\ X_1 - X_20 - 2 >= 0 /\ X_20 >= 0 /\ X_19 + X_20 >= 0 /\ -X_19 + X_20 >= 0 /\ X_18 + X_20 >= 0 /\ -X_18 + X_20 >= 0 /\ X_17 + X_20 >= 0 /\ -X_17 + X_20 >= 0 /\ X_15 + X_20 >= 0 /\ -X_15 + X_20 >= 0 /\ X_12 + X_20 >= 0 /\ -X_12 + X_20 >= 0 /\ X_11 + X_20 >= 0 /\ -X_11 + X_20 >= 0 /\ X_1 + X_20 - 2 >= 0 /\ -X_19 >= 0 /\ X_18 - X_19 >= 0 /\ -X_18 - X_19 >= 0 /\ X_17 - X_19 >= 0 /\ -X_17 - X_19 >= 0 /\ X_15 - X_19 >= 0 /\ -X_15 - X_19 >= 0 /\ X_12 - X_19 >= 0 /\ -X_12 - X_19 >= 0 /\ X_11 - X_19 >= 0 /\ -X_11 - X_19 >= 0 /\ X_1 - X_19 - 2 >= 0 /\ X_19 >= 0 /\ X_18 + X_19 >= 0 /\ -X_18 + X_19 >= 0 /\ X_17 + X_19 >= 0 /\ -X_17 + X_19 >= 0 /\ X_15 + X_19 >= 0 /\ -X_15 + X_19 >= 0 /\ X_12 + X_19 >= 0 /\ -X_12 + X_19 >= 0 /\ X_11 + X_19 >= 0 /\ -X_11 + X_19 >= 0 /\ X_1 + X_19 - 2 >= 0 /\ -X_18 >= 0 /\ X_17 - X_18 >= 0 /\ -X_17 - X_18 >= 0 /\ X_15 - X_18 >= 0 /\ -X_15 - X_18 >= 0 /\ X_12 - X_18 >= 0 /\ -X_12 - X_18 >= 0 /\ X_11 - X_18 >= 0 /\ -X_11 - X_18 >= 0 /\ X_1 - X_18 - 2 >= 0 /\ X_18 >= 0 /\ X_17 + X_18 >= 0 /\ -X_17 + X_18 >= 0 /\ X_15 + X_18 >= 0 /\ -X_15 + X_18 >= 0 /\ X_12 + X_18 >= 0 /\ -X_12 + X_18 >= 0 /\ X_11 + X_18 >= 0 /\ -X_11 + X_18 >= 0 /\ X_1 + X_18 - 2 >= 0 /\ -X_17 >= 0 /\ X_15 - X_17 >= 0 /\ -X_15 - X_17 >= 0 /\ X_12 - X_17 >= 0 /\ -X_12 - X_17 >= 0 /\ X_11 - X_17 >= 0 /\ -X_11 - X_17 >= 0 /\ X_1 - X_17 - 2 >= 0 /\ X_17 >= 0 /\ X_15 + X_17 >= 0 /\ -X_15 + X_17 >= 0 /\ X_12 + X_17 >= 0 /\ -X_12 + X_17 >= 0 /\ X_11 + X_17 >= 0 /\ -X_11 + X_17 >= 0 /\ X_1 + X_17 - 2 >= 0 /\ X_14 - X_16 >= 0 /\ -X_15 >= 0 /\ X_12 - X_15 >= 0 /\ -X_12 - X_15 >= 0 /\ X_11 - X_15 >= 0 /\ -X_11 - X_15 >= 0 /\ X_1 - X_15 - 2 >= 0 /\ X_15 >= 0 /\ X_12 + X_15 >= 0 /\ -X_12 + X_15 >= 0 /\ X_11 + X_15 >= 0 /\ -X_11 + X_15 >= 0 /\ X_1 + X_15 - 2 >= 0 /\ -X_12 >= 0 /\ X_11 - X_12 >= 0 /\ -X_11 - X_12 >= 0 /\ X_1 - X_12 - 2 >= 0 /\ X_12 >= 0 /\ X_11 + X_12 >= 0 /\ -X_11 + X_12 >= 0 /\ X_1 + X_12 - 2 >= 0 /\ -X_11 >= 0 /\ X_1 - X_11 - 2 >= 0 /\ X_11 >= 0 /\ X_1 + X_11 - 2 >= 0 /\ X_1 - 2 >= 0 This yielded the following problem: 7: T: (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(z1, 2, c, e, f, o, 0, z1, s, b2, u, v, s, b1, d1, e1, g1, h1, i1, j1, m1) [ z1 >= 2 /\ s = w ] (2, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f116(a, z1, 0, e, f, o, p, a2, y1, d2, r, r, e2, b1, d1, e1, g1, h1, i1, j1, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(a, b + 1, c, e, f, o, p, q, s, z1, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ b >= 0 /\ q >= b + 1 ] (2, 1) f116(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, e1 + 1, e, f, f, 1, q, r, s, 0, v, w, e1, v, e1, 0, v, 0, v, m1) [ -p >= 0 /\ f - p - 2 >= 0 /\ c - p >= 0 /\ -c - p >= 0 /\ a - p - 2 >= 0 /\ p >= 0 /\ f + p - 2 >= 0 /\ c + p >= 0 /\ -c + p >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ c + f - 2 >= 0 /\ -c + f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ -c >= 0 /\ a - c - 2 >= 0 /\ c >= 0 /\ a + c - 2 >= 0 /\ u - v >= 0 /\ -u + v >= 0 /\ a - 2 >= 0 /\ z1 >= 0 /\ a >= 2 /\ f >= 0 /\ u = 0 /\ p = 0 ] (c + f + e1 + 1, 1) f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, 0, h1, w, b1, d1, e1 - 1, 0, h1, 0, h1, m1) [ -p + 1 >= 0 /\ o - p - 1 >= 0 /\ f - p - 1 >= 0 /\ j1 - p + 1 >= 0 /\ -j1 - p + 1 >= 0 /\ i1 - p + 1 >= 0 /\ -i1 - p + 1 >= 0 /\ h1 - p + 1 >= 0 /\ -h1 - p + 1 >= 0 /\ g1 - p + 1 >= 0 /\ -g1 - p + 1 >= 0 /\ d1 - p + 1 >= 0 /\ -d1 - p + 1 >= 0 /\ v - p + 1 >= 0 /\ -v - p + 1 >= 0 /\ u - p + 1 >= 0 /\ -u - p + 1 >= 0 /\ a - p - 1 >= 0 /\ p - 1 >= 0 /\ o + p - 3 >= 0 /\ f + p - 3 >= 0 /\ j1 + p - 1 >= 0 /\ -j1 + p - 1 >= 0 /\ i1 + p - 1 >= 0 /\ -i1 + p - 1 >= 0 /\ h1 + p - 1 >= 0 /\ -h1 + p - 1 >= 0 /\ g1 + p - 1 >= 0 /\ -g1 + p - 1 >= 0 /\ d1 + p - 1 >= 0 /\ -d1 + p - 1 >= 0 /\ v + p - 1 >= 0 /\ -v + p - 1 >= 0 /\ u + p - 1 >= 0 /\ -u + p - 1 >= 0 /\ a + p - 3 >= 0 /\ f - o >= 0 /\ o - 2 >= 0 /\ f + o - 4 >= 0 /\ -f + o >= 0 /\ j1 + o - 2 >= 0 /\ -j1 + o - 2 >= 0 /\ i1 + o - 2 >= 0 /\ -i1 + o - 2 >= 0 /\ h1 + o - 2 >= 0 /\ -h1 + o - 2 >= 0 /\ g1 + o - 2 >= 0 /\ -g1 + o - 2 >= 0 /\ d1 + o - 2 >= 0 /\ -d1 + o - 2 >= 0 /\ v + o - 2 >= 0 /\ -v + o - 2 >= 0 /\ u + o - 2 >= 0 /\ -u + o - 2 >= 0 /\ a + o - 4 >= 0 /\ -a + o >= 0 /\ f - 2 >= 0 /\ j1 + f - 2 >= 0 /\ -j1 + f - 2 >= 0 /\ i1 + f - 2 >= 0 /\ -i1 + f - 2 >= 0 /\ h1 + f - 2 >= 0 /\ -h1 + f - 2 >= 0 /\ g1 + f - 2 >= 0 /\ -g1 + f - 2 >= 0 /\ d1 + f - 2 >= 0 /\ -d1 + f - 2 >= 0 /\ v + f - 2 >= 0 /\ -v + f - 2 >= 0 /\ u + f - 2 >= 0 /\ -u + f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ b1 - c + 1 >= 0 /\ -e1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -j1 >= 0 /\ i1 - j1 >= 0 /\ -i1 - j1 >= 0 /\ h1 - j1 >= 0 /\ -h1 - j1 >= 0 /\ g1 - j1 >= 0 /\ -g1 - j1 >= 0 /\ d1 - j1 >= 0 /\ -d1 - j1 >= 0 /\ v - j1 >= 0 /\ -v - j1 >= 0 /\ u - j1 >= 0 /\ -u - j1 >= 0 /\ a - j1 - 2 >= 0 /\ j1 >= 0 /\ i1 + j1 >= 0 /\ -i1 + j1 >= 0 /\ h1 + j1 >= 0 /\ -h1 + j1 >= 0 /\ g1 + j1 >= 0 /\ -g1 + j1 >= 0 /\ d1 + j1 >= 0 /\ -d1 + j1 >= 0 /\ v + j1 >= 0 /\ -v + j1 >= 0 /\ u + j1 >= 0 /\ -u + j1 >= 0 /\ a + j1 - 2 >= 0 /\ -i1 >= 0 /\ h1 - i1 >= 0 /\ -h1 - i1 >= 0 /\ g1 - i1 >= 0 /\ -g1 - i1 >= 0 /\ d1 - i1 >= 0 /\ -d1 - i1 >= 0 /\ v - i1 >= 0 /\ -v - i1 >= 0 /\ u - i1 >= 0 /\ -u - i1 >= 0 /\ a - i1 - 2 >= 0 /\ i1 >= 0 /\ h1 + i1 >= 0 /\ -h1 + i1 >= 0 /\ g1 + i1 >= 0 /\ -g1 + i1 >= 0 /\ d1 + i1 >= 0 /\ -d1 + i1 >= 0 /\ v + i1 >= 0 /\ -v + i1 >= 0 /\ u + i1 >= 0 /\ -u + i1 >= 0 /\ a + i1 - 2 >= 0 /\ -h1 >= 0 /\ g1 - h1 >= 0 /\ -g1 - h1 >= 0 /\ d1 - h1 >= 0 /\ -d1 - h1 >= 0 /\ v - h1 >= 0 /\ -v - h1 >= 0 /\ u - h1 >= 0 /\ -u - h1 >= 0 /\ a - h1 - 2 >= 0 /\ h1 >= 0 /\ g1 + h1 >= 0 /\ -g1 + h1 >= 0 /\ d1 + h1 >= 0 /\ -d1 + h1 >= 0 /\ v + h1 >= 0 /\ -v + h1 >= 0 /\ u + h1 >= 0 /\ -u + h1 >= 0 /\ a + h1 - 2 >= 0 /\ -g1 >= 0 /\ d1 - g1 >= 0 /\ -d1 - g1 >= 0 /\ v - g1 >= 0 /\ -v - g1 >= 0 /\ u - g1 >= 0 /\ -u - g1 >= 0 /\ a - g1 - 2 >= 0 /\ g1 >= 0 /\ d1 + g1 >= 0 /\ -d1 + g1 >= 0 /\ v + g1 >= 0 /\ -v + g1 >= 0 /\ u + g1 >= 0 /\ -u + g1 >= 0 /\ a + g1 - 2 >= 0 /\ b1 - e1 >= 0 /\ -d1 >= 0 /\ v - d1 >= 0 /\ -v - d1 >= 0 /\ u - d1 >= 0 /\ -u - d1 >= 0 /\ a - d1 - 2 >= 0 /\ d1 >= 0 /\ v + d1 >= 0 /\ -v + d1 >= 0 /\ u + d1 >= 0 /\ -u + d1 >= 0 /\ a + d1 - 2 >= 0 /\ -v >= 0 /\ u - v >= 0 /\ -u - v >= 0 /\ a - v - 2 >= 0 /\ v >= 0 /\ u + v >= 0 /\ -u + v >= 0 /\ a + v - 2 >= 0 /\ -u >= 0 /\ a - u - 2 >= 0 /\ u >= 0 /\ a + u - 2 >= 0 /\ a - 2 >= 0 /\ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] start location: f9 leaf cost: 6 By chaining the transition f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f116(a, z1, 0, e, f, o, p, a2, y1, d2, r, r, e2, b1, d1, e1, g1, h1, i1, j1, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 ] with all transitions in problem 7, the following new transition is obtained: f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 ] We thus obtain the following problem: 8: T: (2, 2) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 ] (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(z1, 2, c, e, f, o, 0, z1, s, b2, u, v, s, b1, d1, e1, g1, h1, i1, j1, m1) [ z1 >= 2 /\ s = w ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(a, b + 1, c, e, f, o, p, q, s, z1, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ b >= 0 /\ q >= b + 1 ] (2, 1) f116(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, e1 + 1, e, f, f, 1, q, r, s, 0, v, w, e1, v, e1, 0, v, 0, v, m1) [ -p >= 0 /\ f - p - 2 >= 0 /\ c - p >= 0 /\ -c - p >= 0 /\ a - p - 2 >= 0 /\ p >= 0 /\ f + p - 2 >= 0 /\ c + p >= 0 /\ -c + p >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ c + f - 2 >= 0 /\ -c + f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ -c >= 0 /\ a - c - 2 >= 0 /\ c >= 0 /\ a + c - 2 >= 0 /\ u - v >= 0 /\ -u + v >= 0 /\ a - 2 >= 0 /\ z1 >= 0 /\ a >= 2 /\ f >= 0 /\ u = 0 /\ p = 0 ] (c + f + e1 + 1, 1) f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, 0, h1, w, b1, d1, e1 - 1, 0, h1, 0, h1, m1) [ -p + 1 >= 0 /\ o - p - 1 >= 0 /\ f - p - 1 >= 0 /\ j1 - p + 1 >= 0 /\ -j1 - p + 1 >= 0 /\ i1 - p + 1 >= 0 /\ -i1 - p + 1 >= 0 /\ h1 - p + 1 >= 0 /\ -h1 - p + 1 >= 0 /\ g1 - p + 1 >= 0 /\ -g1 - p + 1 >= 0 /\ d1 - p + 1 >= 0 /\ -d1 - p + 1 >= 0 /\ v - p + 1 >= 0 /\ -v - p + 1 >= 0 /\ u - p + 1 >= 0 /\ -u - p + 1 >= 0 /\ a - p - 1 >= 0 /\ p - 1 >= 0 /\ o + p - 3 >= 0 /\ f + p - 3 >= 0 /\ j1 + p - 1 >= 0 /\ -j1 + p - 1 >= 0 /\ i1 + p - 1 >= 0 /\ -i1 + p - 1 >= 0 /\ h1 + p - 1 >= 0 /\ -h1 + p - 1 >= 0 /\ g1 + p - 1 >= 0 /\ -g1 + p - 1 >= 0 /\ d1 + p - 1 >= 0 /\ -d1 + p - 1 >= 0 /\ v + p - 1 >= 0 /\ -v + p - 1 >= 0 /\ u + p - 1 >= 0 /\ -u + p - 1 >= 0 /\ a + p - 3 >= 0 /\ f - o >= 0 /\ o - 2 >= 0 /\ f + o - 4 >= 0 /\ -f + o >= 0 /\ j1 + o - 2 >= 0 /\ -j1 + o - 2 >= 0 /\ i1 + o - 2 >= 0 /\ -i1 + o - 2 >= 0 /\ h1 + o - 2 >= 0 /\ -h1 + o - 2 >= 0 /\ g1 + o - 2 >= 0 /\ -g1 + o - 2 >= 0 /\ d1 + o - 2 >= 0 /\ -d1 + o - 2 >= 0 /\ v + o - 2 >= 0 /\ -v + o - 2 >= 0 /\ u + o - 2 >= 0 /\ -u + o - 2 >= 0 /\ a + o - 4 >= 0 /\ -a + o >= 0 /\ f - 2 >= 0 /\ j1 + f - 2 >= 0 /\ -j1 + f - 2 >= 0 /\ i1 + f - 2 >= 0 /\ -i1 + f - 2 >= 0 /\ h1 + f - 2 >= 0 /\ -h1 + f - 2 >= 0 /\ g1 + f - 2 >= 0 /\ -g1 + f - 2 >= 0 /\ d1 + f - 2 >= 0 /\ -d1 + f - 2 >= 0 /\ v + f - 2 >= 0 /\ -v + f - 2 >= 0 /\ u + f - 2 >= 0 /\ -u + f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ b1 - c + 1 >= 0 /\ -e1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -j1 >= 0 /\ i1 - j1 >= 0 /\ -i1 - j1 >= 0 /\ h1 - j1 >= 0 /\ -h1 - j1 >= 0 /\ g1 - j1 >= 0 /\ -g1 - j1 >= 0 /\ d1 - j1 >= 0 /\ -d1 - j1 >= 0 /\ v - j1 >= 0 /\ -v - j1 >= 0 /\ u - j1 >= 0 /\ -u - j1 >= 0 /\ a - j1 - 2 >= 0 /\ j1 >= 0 /\ i1 + j1 >= 0 /\ -i1 + j1 >= 0 /\ h1 + j1 >= 0 /\ -h1 + j1 >= 0 /\ g1 + j1 >= 0 /\ -g1 + j1 >= 0 /\ d1 + j1 >= 0 /\ -d1 + j1 >= 0 /\ v + j1 >= 0 /\ -v + j1 >= 0 /\ u + j1 >= 0 /\ -u + j1 >= 0 /\ a + j1 - 2 >= 0 /\ -i1 >= 0 /\ h1 - i1 >= 0 /\ -h1 - i1 >= 0 /\ g1 - i1 >= 0 /\ -g1 - i1 >= 0 /\ d1 - i1 >= 0 /\ -d1 - i1 >= 0 /\ v - i1 >= 0 /\ -v - i1 >= 0 /\ u - i1 >= 0 /\ -u - i1 >= 0 /\ a - i1 - 2 >= 0 /\ i1 >= 0 /\ h1 + i1 >= 0 /\ -h1 + i1 >= 0 /\ g1 + i1 >= 0 /\ -g1 + i1 >= 0 /\ d1 + i1 >= 0 /\ -d1 + i1 >= 0 /\ v + i1 >= 0 /\ -v + i1 >= 0 /\ u + i1 >= 0 /\ -u + i1 >= 0 /\ a + i1 - 2 >= 0 /\ -h1 >= 0 /\ g1 - h1 >= 0 /\ -g1 - h1 >= 0 /\ d1 - h1 >= 0 /\ -d1 - h1 >= 0 /\ v - h1 >= 0 /\ -v - h1 >= 0 /\ u - h1 >= 0 /\ -u - h1 >= 0 /\ a - h1 - 2 >= 0 /\ h1 >= 0 /\ g1 + h1 >= 0 /\ -g1 + h1 >= 0 /\ d1 + h1 >= 0 /\ -d1 + h1 >= 0 /\ v + h1 >= 0 /\ -v + h1 >= 0 /\ u + h1 >= 0 /\ -u + h1 >= 0 /\ a + h1 - 2 >= 0 /\ -g1 >= 0 /\ d1 - g1 >= 0 /\ -d1 - g1 >= 0 /\ v - g1 >= 0 /\ -v - g1 >= 0 /\ u - g1 >= 0 /\ -u - g1 >= 0 /\ a - g1 - 2 >= 0 /\ g1 >= 0 /\ d1 + g1 >= 0 /\ -d1 + g1 >= 0 /\ v + g1 >= 0 /\ -v + g1 >= 0 /\ u + g1 >= 0 /\ -u + g1 >= 0 /\ a + g1 - 2 >= 0 /\ b1 - e1 >= 0 /\ -d1 >= 0 /\ v - d1 >= 0 /\ -v - d1 >= 0 /\ u - d1 >= 0 /\ -u - d1 >= 0 /\ a - d1 - 2 >= 0 /\ d1 >= 0 /\ v + d1 >= 0 /\ -v + d1 >= 0 /\ u + d1 >= 0 /\ -u + d1 >= 0 /\ a + d1 - 2 >= 0 /\ -v >= 0 /\ u - v >= 0 /\ -u - v >= 0 /\ a - v - 2 >= 0 /\ v >= 0 /\ u + v >= 0 /\ -u + v >= 0 /\ a + v - 2 >= 0 /\ -u >= 0 /\ a - u - 2 >= 0 /\ u >= 0 /\ a + u - 2 >= 0 /\ a - 2 >= 0 /\ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] start location: f9 leaf cost: 6 Testing for reachability in the complexity graph removes the following transition from problem 8: f116(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, e1 + 1, e, f, f, 1, q, r, s, 0, v, w, e1, v, e1, 0, v, 0, v, m1) [ -p >= 0 /\ f - p - 2 >= 0 /\ c - p >= 0 /\ -c - p >= 0 /\ a - p - 2 >= 0 /\ p >= 0 /\ f + p - 2 >= 0 /\ c + p >= 0 /\ -c + p >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ c + f - 2 >= 0 /\ -c + f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ -c >= 0 /\ a - c - 2 >= 0 /\ c >= 0 /\ a + c - 2 >= 0 /\ u - v >= 0 /\ -u + v >= 0 /\ a - 2 >= 0 /\ z1 >= 0 /\ a >= 2 /\ f >= 0 /\ u = 0 /\ p = 0 ] We thus obtain the following problem: 9: T: (c + f + e1 + 1, 1) f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, 0, h1, w, b1, d1, e1 - 1, 0, h1, 0, h1, m1) [ -p + 1 >= 0 /\ o - p - 1 >= 0 /\ f - p - 1 >= 0 /\ j1 - p + 1 >= 0 /\ -j1 - p + 1 >= 0 /\ i1 - p + 1 >= 0 /\ -i1 - p + 1 >= 0 /\ h1 - p + 1 >= 0 /\ -h1 - p + 1 >= 0 /\ g1 - p + 1 >= 0 /\ -g1 - p + 1 >= 0 /\ d1 - p + 1 >= 0 /\ -d1 - p + 1 >= 0 /\ v - p + 1 >= 0 /\ -v - p + 1 >= 0 /\ u - p + 1 >= 0 /\ -u - p + 1 >= 0 /\ a - p - 1 >= 0 /\ p - 1 >= 0 /\ o + p - 3 >= 0 /\ f + p - 3 >= 0 /\ j1 + p - 1 >= 0 /\ -j1 + p - 1 >= 0 /\ i1 + p - 1 >= 0 /\ -i1 + p - 1 >= 0 /\ h1 + p - 1 >= 0 /\ -h1 + p - 1 >= 0 /\ g1 + p - 1 >= 0 /\ -g1 + p - 1 >= 0 /\ d1 + p - 1 >= 0 /\ -d1 + p - 1 >= 0 /\ v + p - 1 >= 0 /\ -v + p - 1 >= 0 /\ u + p - 1 >= 0 /\ -u + p - 1 >= 0 /\ a + p - 3 >= 0 /\ f - o >= 0 /\ o - 2 >= 0 /\ f + o - 4 >= 0 /\ -f + o >= 0 /\ j1 + o - 2 >= 0 /\ -j1 + o - 2 >= 0 /\ i1 + o - 2 >= 0 /\ -i1 + o - 2 >= 0 /\ h1 + o - 2 >= 0 /\ -h1 + o - 2 >= 0 /\ g1 + o - 2 >= 0 /\ -g1 + o - 2 >= 0 /\ d1 + o - 2 >= 0 /\ -d1 + o - 2 >= 0 /\ v + o - 2 >= 0 /\ -v + o - 2 >= 0 /\ u + o - 2 >= 0 /\ -u + o - 2 >= 0 /\ a + o - 4 >= 0 /\ -a + o >= 0 /\ f - 2 >= 0 /\ j1 + f - 2 >= 0 /\ -j1 + f - 2 >= 0 /\ i1 + f - 2 >= 0 /\ -i1 + f - 2 >= 0 /\ h1 + f - 2 >= 0 /\ -h1 + f - 2 >= 0 /\ g1 + f - 2 >= 0 /\ -g1 + f - 2 >= 0 /\ d1 + f - 2 >= 0 /\ -d1 + f - 2 >= 0 /\ v + f - 2 >= 0 /\ -v + f - 2 >= 0 /\ u + f - 2 >= 0 /\ -u + f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ b1 - c + 1 >= 0 /\ -e1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -j1 >= 0 /\ i1 - j1 >= 0 /\ -i1 - j1 >= 0 /\ h1 - j1 >= 0 /\ -h1 - j1 >= 0 /\ g1 - j1 >= 0 /\ -g1 - j1 >= 0 /\ d1 - j1 >= 0 /\ -d1 - j1 >= 0 /\ v - j1 >= 0 /\ -v - j1 >= 0 /\ u - j1 >= 0 /\ -u - j1 >= 0 /\ a - j1 - 2 >= 0 /\ j1 >= 0 /\ i1 + j1 >= 0 /\ -i1 + j1 >= 0 /\ h1 + j1 >= 0 /\ -h1 + j1 >= 0 /\ g1 + j1 >= 0 /\ -g1 + j1 >= 0 /\ d1 + j1 >= 0 /\ -d1 + j1 >= 0 /\ v + j1 >= 0 /\ -v + j1 >= 0 /\ u + j1 >= 0 /\ -u + j1 >= 0 /\ a + j1 - 2 >= 0 /\ -i1 >= 0 /\ h1 - i1 >= 0 /\ -h1 - i1 >= 0 /\ g1 - i1 >= 0 /\ -g1 - i1 >= 0 /\ d1 - i1 >= 0 /\ -d1 - i1 >= 0 /\ v - i1 >= 0 /\ -v - i1 >= 0 /\ u - i1 >= 0 /\ -u - i1 >= 0 /\ a - i1 - 2 >= 0 /\ i1 >= 0 /\ h1 + i1 >= 0 /\ -h1 + i1 >= 0 /\ g1 + i1 >= 0 /\ -g1 + i1 >= 0 /\ d1 + i1 >= 0 /\ -d1 + i1 >= 0 /\ v + i1 >= 0 /\ -v + i1 >= 0 /\ u + i1 >= 0 /\ -u + i1 >= 0 /\ a + i1 - 2 >= 0 /\ -h1 >= 0 /\ g1 - h1 >= 0 /\ -g1 - h1 >= 0 /\ d1 - h1 >= 0 /\ -d1 - h1 >= 0 /\ v - h1 >= 0 /\ -v - h1 >= 0 /\ u - h1 >= 0 /\ -u - h1 >= 0 /\ a - h1 - 2 >= 0 /\ h1 >= 0 /\ g1 + h1 >= 0 /\ -g1 + h1 >= 0 /\ d1 + h1 >= 0 /\ -d1 + h1 >= 0 /\ v + h1 >= 0 /\ -v + h1 >= 0 /\ u + h1 >= 0 /\ -u + h1 >= 0 /\ a + h1 - 2 >= 0 /\ -g1 >= 0 /\ d1 - g1 >= 0 /\ -d1 - g1 >= 0 /\ v - g1 >= 0 /\ -v - g1 >= 0 /\ u - g1 >= 0 /\ -u - g1 >= 0 /\ a - g1 - 2 >= 0 /\ g1 >= 0 /\ d1 + g1 >= 0 /\ -d1 + g1 >= 0 /\ v + g1 >= 0 /\ -v + g1 >= 0 /\ u + g1 >= 0 /\ -u + g1 >= 0 /\ a + g1 - 2 >= 0 /\ b1 - e1 >= 0 /\ -d1 >= 0 /\ v - d1 >= 0 /\ -v - d1 >= 0 /\ u - d1 >= 0 /\ -u - d1 >= 0 /\ a - d1 - 2 >= 0 /\ d1 >= 0 /\ v + d1 >= 0 /\ -v + d1 >= 0 /\ u + d1 >= 0 /\ -u + d1 >= 0 /\ a + d1 - 2 >= 0 /\ -v >= 0 /\ u - v >= 0 /\ -u - v >= 0 /\ a - v - 2 >= 0 /\ v >= 0 /\ u + v >= 0 /\ -u + v >= 0 /\ a + v - 2 >= 0 /\ -u >= 0 /\ a - u - 2 >= 0 /\ u >= 0 /\ a + u - 2 >= 0 /\ a - 2 >= 0 /\ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] (2, 2) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(a, b + 1, c, e, f, o, p, q, s, z1, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ b >= 0 /\ q >= b + 1 ] (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(z1, 2, c, e, f, o, 0, z1, s, b2, u, v, s, b1, d1, e1, g1, h1, i1, j1, m1) [ z1 >= 2 /\ s = w ] start location: f9 leaf cost: 6 By chaining the transition f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 ] with all transitions in problem 9, the following new transition is obtained: f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 1, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r ] We thus obtain the following problem: 10: T: (2, 3) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 1, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r ] (c + f + e1 + 1, 1) f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, 0, h1, w, b1, d1, e1 - 1, 0, h1, 0, h1, m1) [ -p + 1 >= 0 /\ o - p - 1 >= 0 /\ f - p - 1 >= 0 /\ j1 - p + 1 >= 0 /\ -j1 - p + 1 >= 0 /\ i1 - p + 1 >= 0 /\ -i1 - p + 1 >= 0 /\ h1 - p + 1 >= 0 /\ -h1 - p + 1 >= 0 /\ g1 - p + 1 >= 0 /\ -g1 - p + 1 >= 0 /\ d1 - p + 1 >= 0 /\ -d1 - p + 1 >= 0 /\ v - p + 1 >= 0 /\ -v - p + 1 >= 0 /\ u - p + 1 >= 0 /\ -u - p + 1 >= 0 /\ a - p - 1 >= 0 /\ p - 1 >= 0 /\ o + p - 3 >= 0 /\ f + p - 3 >= 0 /\ j1 + p - 1 >= 0 /\ -j1 + p - 1 >= 0 /\ i1 + p - 1 >= 0 /\ -i1 + p - 1 >= 0 /\ h1 + p - 1 >= 0 /\ -h1 + p - 1 >= 0 /\ g1 + p - 1 >= 0 /\ -g1 + p - 1 >= 0 /\ d1 + p - 1 >= 0 /\ -d1 + p - 1 >= 0 /\ v + p - 1 >= 0 /\ -v + p - 1 >= 0 /\ u + p - 1 >= 0 /\ -u + p - 1 >= 0 /\ a + p - 3 >= 0 /\ f - o >= 0 /\ o - 2 >= 0 /\ f + o - 4 >= 0 /\ -f + o >= 0 /\ j1 + o - 2 >= 0 /\ -j1 + o - 2 >= 0 /\ i1 + o - 2 >= 0 /\ -i1 + o - 2 >= 0 /\ h1 + o - 2 >= 0 /\ -h1 + o - 2 >= 0 /\ g1 + o - 2 >= 0 /\ -g1 + o - 2 >= 0 /\ d1 + o - 2 >= 0 /\ -d1 + o - 2 >= 0 /\ v + o - 2 >= 0 /\ -v + o - 2 >= 0 /\ u + o - 2 >= 0 /\ -u + o - 2 >= 0 /\ a + o - 4 >= 0 /\ -a + o >= 0 /\ f - 2 >= 0 /\ j1 + f - 2 >= 0 /\ -j1 + f - 2 >= 0 /\ i1 + f - 2 >= 0 /\ -i1 + f - 2 >= 0 /\ h1 + f - 2 >= 0 /\ -h1 + f - 2 >= 0 /\ g1 + f - 2 >= 0 /\ -g1 + f - 2 >= 0 /\ d1 + f - 2 >= 0 /\ -d1 + f - 2 >= 0 /\ v + f - 2 >= 0 /\ -v + f - 2 >= 0 /\ u + f - 2 >= 0 /\ -u + f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ b1 - c + 1 >= 0 /\ -e1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -j1 >= 0 /\ i1 - j1 >= 0 /\ -i1 - j1 >= 0 /\ h1 - j1 >= 0 /\ -h1 - j1 >= 0 /\ g1 - j1 >= 0 /\ -g1 - j1 >= 0 /\ d1 - j1 >= 0 /\ -d1 - j1 >= 0 /\ v - j1 >= 0 /\ -v - j1 >= 0 /\ u - j1 >= 0 /\ -u - j1 >= 0 /\ a - j1 - 2 >= 0 /\ j1 >= 0 /\ i1 + j1 >= 0 /\ -i1 + j1 >= 0 /\ h1 + j1 >= 0 /\ -h1 + j1 >= 0 /\ g1 + j1 >= 0 /\ -g1 + j1 >= 0 /\ d1 + j1 >= 0 /\ -d1 + j1 >= 0 /\ v + j1 >= 0 /\ -v + j1 >= 0 /\ u + j1 >= 0 /\ -u + j1 >= 0 /\ a + j1 - 2 >= 0 /\ -i1 >= 0 /\ h1 - i1 >= 0 /\ -h1 - i1 >= 0 /\ g1 - i1 >= 0 /\ -g1 - i1 >= 0 /\ d1 - i1 >= 0 /\ -d1 - i1 >= 0 /\ v - i1 >= 0 /\ -v - i1 >= 0 /\ u - i1 >= 0 /\ -u - i1 >= 0 /\ a - i1 - 2 >= 0 /\ i1 >= 0 /\ h1 + i1 >= 0 /\ -h1 + i1 >= 0 /\ g1 + i1 >= 0 /\ -g1 + i1 >= 0 /\ d1 + i1 >= 0 /\ -d1 + i1 >= 0 /\ v + i1 >= 0 /\ -v + i1 >= 0 /\ u + i1 >= 0 /\ -u + i1 >= 0 /\ a + i1 - 2 >= 0 /\ -h1 >= 0 /\ g1 - h1 >= 0 /\ -g1 - h1 >= 0 /\ d1 - h1 >= 0 /\ -d1 - h1 >= 0 /\ v - h1 >= 0 /\ -v - h1 >= 0 /\ u - h1 >= 0 /\ -u - h1 >= 0 /\ a - h1 - 2 >= 0 /\ h1 >= 0 /\ g1 + h1 >= 0 /\ -g1 + h1 >= 0 /\ d1 + h1 >= 0 /\ -d1 + h1 >= 0 /\ v + h1 >= 0 /\ -v + h1 >= 0 /\ u + h1 >= 0 /\ -u + h1 >= 0 /\ a + h1 - 2 >= 0 /\ -g1 >= 0 /\ d1 - g1 >= 0 /\ -d1 - g1 >= 0 /\ v - g1 >= 0 /\ -v - g1 >= 0 /\ u - g1 >= 0 /\ -u - g1 >= 0 /\ a - g1 - 2 >= 0 /\ g1 >= 0 /\ d1 + g1 >= 0 /\ -d1 + g1 >= 0 /\ v + g1 >= 0 /\ -v + g1 >= 0 /\ u + g1 >= 0 /\ -u + g1 >= 0 /\ a + g1 - 2 >= 0 /\ b1 - e1 >= 0 /\ -d1 >= 0 /\ v - d1 >= 0 /\ -v - d1 >= 0 /\ u - d1 >= 0 /\ -u - d1 >= 0 /\ a - d1 - 2 >= 0 /\ d1 >= 0 /\ v + d1 >= 0 /\ -v + d1 >= 0 /\ u + d1 >= 0 /\ -u + d1 >= 0 /\ a + d1 - 2 >= 0 /\ -v >= 0 /\ u - v >= 0 /\ -u - v >= 0 /\ a - v - 2 >= 0 /\ v >= 0 /\ u + v >= 0 /\ -u + v >= 0 /\ a + v - 2 >= 0 /\ -u >= 0 /\ a - u - 2 >= 0 /\ u >= 0 /\ a + u - 2 >= 0 /\ a - 2 >= 0 /\ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(a, b + 1, c, e, f, o, p, q, s, z1, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ b >= 0 /\ q >= b + 1 ] (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(z1, 2, c, e, f, o, 0, z1, s, b2, u, v, s, b1, d1, e1, g1, h1, i1, j1, m1) [ z1 >= 2 /\ s = w ] start location: f9 leaf cost: 6 By chaining the transition f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 1, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r ] with all transitions in problem 10, the following new transition is obtained: f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 2, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 ] We thus obtain the following problem: 11: T: (2, 4) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 2, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 ] (c + f + e1 + 1, 1) f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, 0, h1, w, b1, d1, e1 - 1, 0, h1, 0, h1, m1) [ -p + 1 >= 0 /\ o - p - 1 >= 0 /\ f - p - 1 >= 0 /\ j1 - p + 1 >= 0 /\ -j1 - p + 1 >= 0 /\ i1 - p + 1 >= 0 /\ -i1 - p + 1 >= 0 /\ h1 - p + 1 >= 0 /\ -h1 - p + 1 >= 0 /\ g1 - p + 1 >= 0 /\ -g1 - p + 1 >= 0 /\ d1 - p + 1 >= 0 /\ -d1 - p + 1 >= 0 /\ v - p + 1 >= 0 /\ -v - p + 1 >= 0 /\ u - p + 1 >= 0 /\ -u - p + 1 >= 0 /\ a - p - 1 >= 0 /\ p - 1 >= 0 /\ o + p - 3 >= 0 /\ f + p - 3 >= 0 /\ j1 + p - 1 >= 0 /\ -j1 + p - 1 >= 0 /\ i1 + p - 1 >= 0 /\ -i1 + p - 1 >= 0 /\ h1 + p - 1 >= 0 /\ -h1 + p - 1 >= 0 /\ g1 + p - 1 >= 0 /\ -g1 + p - 1 >= 0 /\ d1 + p - 1 >= 0 /\ -d1 + p - 1 >= 0 /\ v + p - 1 >= 0 /\ -v + p - 1 >= 0 /\ u + p - 1 >= 0 /\ -u + p - 1 >= 0 /\ a + p - 3 >= 0 /\ f - o >= 0 /\ o - 2 >= 0 /\ f + o - 4 >= 0 /\ -f + o >= 0 /\ j1 + o - 2 >= 0 /\ -j1 + o - 2 >= 0 /\ i1 + o - 2 >= 0 /\ -i1 + o - 2 >= 0 /\ h1 + o - 2 >= 0 /\ -h1 + o - 2 >= 0 /\ g1 + o - 2 >= 0 /\ -g1 + o - 2 >= 0 /\ d1 + o - 2 >= 0 /\ -d1 + o - 2 >= 0 /\ v + o - 2 >= 0 /\ -v + o - 2 >= 0 /\ u + o - 2 >= 0 /\ -u + o - 2 >= 0 /\ a + o - 4 >= 0 /\ -a + o >= 0 /\ f - 2 >= 0 /\ j1 + f - 2 >= 0 /\ -j1 + f - 2 >= 0 /\ i1 + f - 2 >= 0 /\ -i1 + f - 2 >= 0 /\ h1 + f - 2 >= 0 /\ -h1 + f - 2 >= 0 /\ g1 + f - 2 >= 0 /\ -g1 + f - 2 >= 0 /\ d1 + f - 2 >= 0 /\ -d1 + f - 2 >= 0 /\ v + f - 2 >= 0 /\ -v + f - 2 >= 0 /\ u + f - 2 >= 0 /\ -u + f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ b1 - c + 1 >= 0 /\ -e1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -j1 >= 0 /\ i1 - j1 >= 0 /\ -i1 - j1 >= 0 /\ h1 - j1 >= 0 /\ -h1 - j1 >= 0 /\ g1 - j1 >= 0 /\ -g1 - j1 >= 0 /\ d1 - j1 >= 0 /\ -d1 - j1 >= 0 /\ v - j1 >= 0 /\ -v - j1 >= 0 /\ u - j1 >= 0 /\ -u - j1 >= 0 /\ a - j1 - 2 >= 0 /\ j1 >= 0 /\ i1 + j1 >= 0 /\ -i1 + j1 >= 0 /\ h1 + j1 >= 0 /\ -h1 + j1 >= 0 /\ g1 + j1 >= 0 /\ -g1 + j1 >= 0 /\ d1 + j1 >= 0 /\ -d1 + j1 >= 0 /\ v + j1 >= 0 /\ -v + j1 >= 0 /\ u + j1 >= 0 /\ -u + j1 >= 0 /\ a + j1 - 2 >= 0 /\ -i1 >= 0 /\ h1 - i1 >= 0 /\ -h1 - i1 >= 0 /\ g1 - i1 >= 0 /\ -g1 - i1 >= 0 /\ d1 - i1 >= 0 /\ -d1 - i1 >= 0 /\ v - i1 >= 0 /\ -v - i1 >= 0 /\ u - i1 >= 0 /\ -u - i1 >= 0 /\ a - i1 - 2 >= 0 /\ i1 >= 0 /\ h1 + i1 >= 0 /\ -h1 + i1 >= 0 /\ g1 + i1 >= 0 /\ -g1 + i1 >= 0 /\ d1 + i1 >= 0 /\ -d1 + i1 >= 0 /\ v + i1 >= 0 /\ -v + i1 >= 0 /\ u + i1 >= 0 /\ -u + i1 >= 0 /\ a + i1 - 2 >= 0 /\ -h1 >= 0 /\ g1 - h1 >= 0 /\ -g1 - h1 >= 0 /\ d1 - h1 >= 0 /\ -d1 - h1 >= 0 /\ v - h1 >= 0 /\ -v - h1 >= 0 /\ u - h1 >= 0 /\ -u - h1 >= 0 /\ a - h1 - 2 >= 0 /\ h1 >= 0 /\ g1 + h1 >= 0 /\ -g1 + h1 >= 0 /\ d1 + h1 >= 0 /\ -d1 + h1 >= 0 /\ v + h1 >= 0 /\ -v + h1 >= 0 /\ u + h1 >= 0 /\ -u + h1 >= 0 /\ a + h1 - 2 >= 0 /\ -g1 >= 0 /\ d1 - g1 >= 0 /\ -d1 - g1 >= 0 /\ v - g1 >= 0 /\ -v - g1 >= 0 /\ u - g1 >= 0 /\ -u - g1 >= 0 /\ a - g1 - 2 >= 0 /\ g1 >= 0 /\ d1 + g1 >= 0 /\ -d1 + g1 >= 0 /\ v + g1 >= 0 /\ -v + g1 >= 0 /\ u + g1 >= 0 /\ -u + g1 >= 0 /\ a + g1 - 2 >= 0 /\ b1 - e1 >= 0 /\ -d1 >= 0 /\ v - d1 >= 0 /\ -v - d1 >= 0 /\ u - d1 >= 0 /\ -u - d1 >= 0 /\ a - d1 - 2 >= 0 /\ d1 >= 0 /\ v + d1 >= 0 /\ -v + d1 >= 0 /\ u + d1 >= 0 /\ -u + d1 >= 0 /\ a + d1 - 2 >= 0 /\ -v >= 0 /\ u - v >= 0 /\ -u - v >= 0 /\ a - v - 2 >= 0 /\ v >= 0 /\ u + v >= 0 /\ -u + v >= 0 /\ a + v - 2 >= 0 /\ -u >= 0 /\ a - u - 2 >= 0 /\ u >= 0 /\ a + u - 2 >= 0 /\ a - 2 >= 0 /\ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(a, b + 1, c, e, f, o, p, q, s, z1, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ b >= 0 /\ q >= b + 1 ] (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(z1, 2, c, e, f, o, 0, z1, s, b2, u, v, s, b1, d1, e1, g1, h1, i1, j1, m1) [ z1 >= 2 /\ s = w ] start location: f9 leaf cost: 6 By chaining the transition f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 2, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 ] with all transitions in problem 11, the following new transition is obtained: f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 3, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 ] We thus obtain the following problem: 12: T: (2, 5) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 3, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 ] (c + f + e1 + 1, 1) f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, 0, h1, w, b1, d1, e1 - 1, 0, h1, 0, h1, m1) [ -p + 1 >= 0 /\ o - p - 1 >= 0 /\ f - p - 1 >= 0 /\ j1 - p + 1 >= 0 /\ -j1 - p + 1 >= 0 /\ i1 - p + 1 >= 0 /\ -i1 - p + 1 >= 0 /\ h1 - p + 1 >= 0 /\ -h1 - p + 1 >= 0 /\ g1 - p + 1 >= 0 /\ -g1 - p + 1 >= 0 /\ d1 - p + 1 >= 0 /\ -d1 - p + 1 >= 0 /\ v - p + 1 >= 0 /\ -v - p + 1 >= 0 /\ u - p + 1 >= 0 /\ -u - p + 1 >= 0 /\ a - p - 1 >= 0 /\ p - 1 >= 0 /\ o + p - 3 >= 0 /\ f + p - 3 >= 0 /\ j1 + p - 1 >= 0 /\ -j1 + p - 1 >= 0 /\ i1 + p - 1 >= 0 /\ -i1 + p - 1 >= 0 /\ h1 + p - 1 >= 0 /\ -h1 + p - 1 >= 0 /\ g1 + p - 1 >= 0 /\ -g1 + p - 1 >= 0 /\ d1 + p - 1 >= 0 /\ -d1 + p - 1 >= 0 /\ v + p - 1 >= 0 /\ -v + p - 1 >= 0 /\ u + p - 1 >= 0 /\ -u + p - 1 >= 0 /\ a + p - 3 >= 0 /\ f - o >= 0 /\ o - 2 >= 0 /\ f + o - 4 >= 0 /\ -f + o >= 0 /\ j1 + o - 2 >= 0 /\ -j1 + o - 2 >= 0 /\ i1 + o - 2 >= 0 /\ -i1 + o - 2 >= 0 /\ h1 + o - 2 >= 0 /\ -h1 + o - 2 >= 0 /\ g1 + o - 2 >= 0 /\ -g1 + o - 2 >= 0 /\ d1 + o - 2 >= 0 /\ -d1 + o - 2 >= 0 /\ v + o - 2 >= 0 /\ -v + o - 2 >= 0 /\ u + o - 2 >= 0 /\ -u + o - 2 >= 0 /\ a + o - 4 >= 0 /\ -a + o >= 0 /\ f - 2 >= 0 /\ j1 + f - 2 >= 0 /\ -j1 + f - 2 >= 0 /\ i1 + f - 2 >= 0 /\ -i1 + f - 2 >= 0 /\ h1 + f - 2 >= 0 /\ -h1 + f - 2 >= 0 /\ g1 + f - 2 >= 0 /\ -g1 + f - 2 >= 0 /\ d1 + f - 2 >= 0 /\ -d1 + f - 2 >= 0 /\ v + f - 2 >= 0 /\ -v + f - 2 >= 0 /\ u + f - 2 >= 0 /\ -u + f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ b1 - c + 1 >= 0 /\ -e1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -j1 >= 0 /\ i1 - j1 >= 0 /\ -i1 - j1 >= 0 /\ h1 - j1 >= 0 /\ -h1 - j1 >= 0 /\ g1 - j1 >= 0 /\ -g1 - j1 >= 0 /\ d1 - j1 >= 0 /\ -d1 - j1 >= 0 /\ v - j1 >= 0 /\ -v - j1 >= 0 /\ u - j1 >= 0 /\ -u - j1 >= 0 /\ a - j1 - 2 >= 0 /\ j1 >= 0 /\ i1 + j1 >= 0 /\ -i1 + j1 >= 0 /\ h1 + j1 >= 0 /\ -h1 + j1 >= 0 /\ g1 + j1 >= 0 /\ -g1 + j1 >= 0 /\ d1 + j1 >= 0 /\ -d1 + j1 >= 0 /\ v + j1 >= 0 /\ -v + j1 >= 0 /\ u + j1 >= 0 /\ -u + j1 >= 0 /\ a + j1 - 2 >= 0 /\ -i1 >= 0 /\ h1 - i1 >= 0 /\ -h1 - i1 >= 0 /\ g1 - i1 >= 0 /\ -g1 - i1 >= 0 /\ d1 - i1 >= 0 /\ -d1 - i1 >= 0 /\ v - i1 >= 0 /\ -v - i1 >= 0 /\ u - i1 >= 0 /\ -u - i1 >= 0 /\ a - i1 - 2 >= 0 /\ i1 >= 0 /\ h1 + i1 >= 0 /\ -h1 + i1 >= 0 /\ g1 + i1 >= 0 /\ -g1 + i1 >= 0 /\ d1 + i1 >= 0 /\ -d1 + i1 >= 0 /\ v + i1 >= 0 /\ -v + i1 >= 0 /\ u + i1 >= 0 /\ -u + i1 >= 0 /\ a + i1 - 2 >= 0 /\ -h1 >= 0 /\ g1 - h1 >= 0 /\ -g1 - h1 >= 0 /\ d1 - h1 >= 0 /\ -d1 - h1 >= 0 /\ v - h1 >= 0 /\ -v - h1 >= 0 /\ u - h1 >= 0 /\ -u - h1 >= 0 /\ a - h1 - 2 >= 0 /\ h1 >= 0 /\ g1 + h1 >= 0 /\ -g1 + h1 >= 0 /\ d1 + h1 >= 0 /\ -d1 + h1 >= 0 /\ v + h1 >= 0 /\ -v + h1 >= 0 /\ u + h1 >= 0 /\ -u + h1 >= 0 /\ a + h1 - 2 >= 0 /\ -g1 >= 0 /\ d1 - g1 >= 0 /\ -d1 - g1 >= 0 /\ v - g1 >= 0 /\ -v - g1 >= 0 /\ u - g1 >= 0 /\ -u - g1 >= 0 /\ a - g1 - 2 >= 0 /\ g1 >= 0 /\ d1 + g1 >= 0 /\ -d1 + g1 >= 0 /\ v + g1 >= 0 /\ -v + g1 >= 0 /\ u + g1 >= 0 /\ -u + g1 >= 0 /\ a + g1 - 2 >= 0 /\ b1 - e1 >= 0 /\ -d1 >= 0 /\ v - d1 >= 0 /\ -v - d1 >= 0 /\ u - d1 >= 0 /\ -u - d1 >= 0 /\ a - d1 - 2 >= 0 /\ d1 >= 0 /\ v + d1 >= 0 /\ -v + d1 >= 0 /\ u + d1 >= 0 /\ -u + d1 >= 0 /\ a + d1 - 2 >= 0 /\ -v >= 0 /\ u - v >= 0 /\ -u - v >= 0 /\ a - v - 2 >= 0 /\ v >= 0 /\ u + v >= 0 /\ -u + v >= 0 /\ a + v - 2 >= 0 /\ -u >= 0 /\ a - u - 2 >= 0 /\ u >= 0 /\ a + u - 2 >= 0 /\ a - 2 >= 0 /\ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(a, b + 1, c, e, f, o, p, q, s, z1, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ b >= 0 /\ q >= b + 1 ] (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(z1, 2, c, e, f, o, 0, z1, s, b2, u, v, s, b1, d1, e1, g1, h1, i1, j1, m1) [ z1 >= 2 /\ s = w ] start location: f9 leaf cost: 6 By chaining the transition f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 3, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 ] with all transitions in problem 12, the following new transition is obtained: f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 4, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 ] We thus obtain the following problem: 13: T: (2, 6) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 4, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 ] (c + f + e1 + 1, 1) f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, 0, h1, w, b1, d1, e1 - 1, 0, h1, 0, h1, m1) [ -p + 1 >= 0 /\ o - p - 1 >= 0 /\ f - p - 1 >= 0 /\ j1 - p + 1 >= 0 /\ -j1 - p + 1 >= 0 /\ i1 - p + 1 >= 0 /\ -i1 - p + 1 >= 0 /\ h1 - p + 1 >= 0 /\ -h1 - p + 1 >= 0 /\ g1 - p + 1 >= 0 /\ -g1 - p + 1 >= 0 /\ d1 - p + 1 >= 0 /\ -d1 - p + 1 >= 0 /\ v - p + 1 >= 0 /\ -v - p + 1 >= 0 /\ u - p + 1 >= 0 /\ -u - p + 1 >= 0 /\ a - p - 1 >= 0 /\ p - 1 >= 0 /\ o + p - 3 >= 0 /\ f + p - 3 >= 0 /\ j1 + p - 1 >= 0 /\ -j1 + p - 1 >= 0 /\ i1 + p - 1 >= 0 /\ -i1 + p - 1 >= 0 /\ h1 + p - 1 >= 0 /\ -h1 + p - 1 >= 0 /\ g1 + p - 1 >= 0 /\ -g1 + p - 1 >= 0 /\ d1 + p - 1 >= 0 /\ -d1 + p - 1 >= 0 /\ v + p - 1 >= 0 /\ -v + p - 1 >= 0 /\ u + p - 1 >= 0 /\ -u + p - 1 >= 0 /\ a + p - 3 >= 0 /\ f - o >= 0 /\ o - 2 >= 0 /\ f + o - 4 >= 0 /\ -f + o >= 0 /\ j1 + o - 2 >= 0 /\ -j1 + o - 2 >= 0 /\ i1 + o - 2 >= 0 /\ -i1 + o - 2 >= 0 /\ h1 + o - 2 >= 0 /\ -h1 + o - 2 >= 0 /\ g1 + o - 2 >= 0 /\ -g1 + o - 2 >= 0 /\ d1 + o - 2 >= 0 /\ -d1 + o - 2 >= 0 /\ v + o - 2 >= 0 /\ -v + o - 2 >= 0 /\ u + o - 2 >= 0 /\ -u + o - 2 >= 0 /\ a + o - 4 >= 0 /\ -a + o >= 0 /\ f - 2 >= 0 /\ j1 + f - 2 >= 0 /\ -j1 + f - 2 >= 0 /\ i1 + f - 2 >= 0 /\ -i1 + f - 2 >= 0 /\ h1 + f - 2 >= 0 /\ -h1 + f - 2 >= 0 /\ g1 + f - 2 >= 0 /\ -g1 + f - 2 >= 0 /\ d1 + f - 2 >= 0 /\ -d1 + f - 2 >= 0 /\ v + f - 2 >= 0 /\ -v + f - 2 >= 0 /\ u + f - 2 >= 0 /\ -u + f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ b1 - c + 1 >= 0 /\ -e1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -j1 >= 0 /\ i1 - j1 >= 0 /\ -i1 - j1 >= 0 /\ h1 - j1 >= 0 /\ -h1 - j1 >= 0 /\ g1 - j1 >= 0 /\ -g1 - j1 >= 0 /\ d1 - j1 >= 0 /\ -d1 - j1 >= 0 /\ v - j1 >= 0 /\ -v - j1 >= 0 /\ u - j1 >= 0 /\ -u - j1 >= 0 /\ a - j1 - 2 >= 0 /\ j1 >= 0 /\ i1 + j1 >= 0 /\ -i1 + j1 >= 0 /\ h1 + j1 >= 0 /\ -h1 + j1 >= 0 /\ g1 + j1 >= 0 /\ -g1 + j1 >= 0 /\ d1 + j1 >= 0 /\ -d1 + j1 >= 0 /\ v + j1 >= 0 /\ -v + j1 >= 0 /\ u + j1 >= 0 /\ -u + j1 >= 0 /\ a + j1 - 2 >= 0 /\ -i1 >= 0 /\ h1 - i1 >= 0 /\ -h1 - i1 >= 0 /\ g1 - i1 >= 0 /\ -g1 - i1 >= 0 /\ d1 - i1 >= 0 /\ -d1 - i1 >= 0 /\ v - i1 >= 0 /\ -v - i1 >= 0 /\ u - i1 >= 0 /\ -u - i1 >= 0 /\ a - i1 - 2 >= 0 /\ i1 >= 0 /\ h1 + i1 >= 0 /\ -h1 + i1 >= 0 /\ g1 + i1 >= 0 /\ -g1 + i1 >= 0 /\ d1 + i1 >= 0 /\ -d1 + i1 >= 0 /\ v + i1 >= 0 /\ -v + i1 >= 0 /\ u + i1 >= 0 /\ -u + i1 >= 0 /\ a + i1 - 2 >= 0 /\ -h1 >= 0 /\ g1 - h1 >= 0 /\ -g1 - h1 >= 0 /\ d1 - h1 >= 0 /\ -d1 - h1 >= 0 /\ v - h1 >= 0 /\ -v - h1 >= 0 /\ u - h1 >= 0 /\ -u - h1 >= 0 /\ a - h1 - 2 >= 0 /\ h1 >= 0 /\ g1 + h1 >= 0 /\ -g1 + h1 >= 0 /\ d1 + h1 >= 0 /\ -d1 + h1 >= 0 /\ v + h1 >= 0 /\ -v + h1 >= 0 /\ u + h1 >= 0 /\ -u + h1 >= 0 /\ a + h1 - 2 >= 0 /\ -g1 >= 0 /\ d1 - g1 >= 0 /\ -d1 - g1 >= 0 /\ v - g1 >= 0 /\ -v - g1 >= 0 /\ u - g1 >= 0 /\ -u - g1 >= 0 /\ a - g1 - 2 >= 0 /\ g1 >= 0 /\ d1 + g1 >= 0 /\ -d1 + g1 >= 0 /\ v + g1 >= 0 /\ -v + g1 >= 0 /\ u + g1 >= 0 /\ -u + g1 >= 0 /\ a + g1 - 2 >= 0 /\ b1 - e1 >= 0 /\ -d1 >= 0 /\ v - d1 >= 0 /\ -v - d1 >= 0 /\ u - d1 >= 0 /\ -u - d1 >= 0 /\ a - d1 - 2 >= 0 /\ d1 >= 0 /\ v + d1 >= 0 /\ -v + d1 >= 0 /\ u + d1 >= 0 /\ -u + d1 >= 0 /\ a + d1 - 2 >= 0 /\ -v >= 0 /\ u - v >= 0 /\ -u - v >= 0 /\ a - v - 2 >= 0 /\ v >= 0 /\ u + v >= 0 /\ -u + v >= 0 /\ a + v - 2 >= 0 /\ -u >= 0 /\ a - u - 2 >= 0 /\ u >= 0 /\ a + u - 2 >= 0 /\ a - 2 >= 0 /\ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(a, b + 1, c, e, f, o, p, q, s, z1, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ b >= 0 /\ q >= b + 1 ] (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(z1, 2, c, e, f, o, 0, z1, s, b2, u, v, s, b1, d1, e1, g1, h1, i1, j1, m1) [ z1 >= 2 /\ s = w ] start location: f9 leaf cost: 6 By chaining the transition f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 4, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 ] with all transitions in problem 13, the following new transition is obtained: f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 5, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 ] We thus obtain the following problem: 14: T: (2, 7) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 5, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 ] (c + f + e1 + 1, 1) f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, 0, h1, w, b1, d1, e1 - 1, 0, h1, 0, h1, m1) [ -p + 1 >= 0 /\ o - p - 1 >= 0 /\ f - p - 1 >= 0 /\ j1 - p + 1 >= 0 /\ -j1 - p + 1 >= 0 /\ i1 - p + 1 >= 0 /\ -i1 - p + 1 >= 0 /\ h1 - p + 1 >= 0 /\ -h1 - p + 1 >= 0 /\ g1 - p + 1 >= 0 /\ -g1 - p + 1 >= 0 /\ d1 - p + 1 >= 0 /\ -d1 - p + 1 >= 0 /\ v - p + 1 >= 0 /\ -v - p + 1 >= 0 /\ u - p + 1 >= 0 /\ -u - p + 1 >= 0 /\ a - p - 1 >= 0 /\ p - 1 >= 0 /\ o + p - 3 >= 0 /\ f + p - 3 >= 0 /\ j1 + p - 1 >= 0 /\ -j1 + p - 1 >= 0 /\ i1 + p - 1 >= 0 /\ -i1 + p - 1 >= 0 /\ h1 + p - 1 >= 0 /\ -h1 + p - 1 >= 0 /\ g1 + p - 1 >= 0 /\ -g1 + p - 1 >= 0 /\ d1 + p - 1 >= 0 /\ -d1 + p - 1 >= 0 /\ v + p - 1 >= 0 /\ -v + p - 1 >= 0 /\ u + p - 1 >= 0 /\ -u + p - 1 >= 0 /\ a + p - 3 >= 0 /\ f - o >= 0 /\ o - 2 >= 0 /\ f + o - 4 >= 0 /\ -f + o >= 0 /\ j1 + o - 2 >= 0 /\ -j1 + o - 2 >= 0 /\ i1 + o - 2 >= 0 /\ -i1 + o - 2 >= 0 /\ h1 + o - 2 >= 0 /\ -h1 + o - 2 >= 0 /\ g1 + o - 2 >= 0 /\ -g1 + o - 2 >= 0 /\ d1 + o - 2 >= 0 /\ -d1 + o - 2 >= 0 /\ v + o - 2 >= 0 /\ -v + o - 2 >= 0 /\ u + o - 2 >= 0 /\ -u + o - 2 >= 0 /\ a + o - 4 >= 0 /\ -a + o >= 0 /\ f - 2 >= 0 /\ j1 + f - 2 >= 0 /\ -j1 + f - 2 >= 0 /\ i1 + f - 2 >= 0 /\ -i1 + f - 2 >= 0 /\ h1 + f - 2 >= 0 /\ -h1 + f - 2 >= 0 /\ g1 + f - 2 >= 0 /\ -g1 + f - 2 >= 0 /\ d1 + f - 2 >= 0 /\ -d1 + f - 2 >= 0 /\ v + f - 2 >= 0 /\ -v + f - 2 >= 0 /\ u + f - 2 >= 0 /\ -u + f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ b1 - c + 1 >= 0 /\ -e1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -j1 >= 0 /\ i1 - j1 >= 0 /\ -i1 - j1 >= 0 /\ h1 - j1 >= 0 /\ -h1 - j1 >= 0 /\ g1 - j1 >= 0 /\ -g1 - j1 >= 0 /\ d1 - j1 >= 0 /\ -d1 - j1 >= 0 /\ v - j1 >= 0 /\ -v - j1 >= 0 /\ u - j1 >= 0 /\ -u - j1 >= 0 /\ a - j1 - 2 >= 0 /\ j1 >= 0 /\ i1 + j1 >= 0 /\ -i1 + j1 >= 0 /\ h1 + j1 >= 0 /\ -h1 + j1 >= 0 /\ g1 + j1 >= 0 /\ -g1 + j1 >= 0 /\ d1 + j1 >= 0 /\ -d1 + j1 >= 0 /\ v + j1 >= 0 /\ -v + j1 >= 0 /\ u + j1 >= 0 /\ -u + j1 >= 0 /\ a + j1 - 2 >= 0 /\ -i1 >= 0 /\ h1 - i1 >= 0 /\ -h1 - i1 >= 0 /\ g1 - i1 >= 0 /\ -g1 - i1 >= 0 /\ d1 - i1 >= 0 /\ -d1 - i1 >= 0 /\ v - i1 >= 0 /\ -v - i1 >= 0 /\ u - i1 >= 0 /\ -u - i1 >= 0 /\ a - i1 - 2 >= 0 /\ i1 >= 0 /\ h1 + i1 >= 0 /\ -h1 + i1 >= 0 /\ g1 + i1 >= 0 /\ -g1 + i1 >= 0 /\ d1 + i1 >= 0 /\ -d1 + i1 >= 0 /\ v + i1 >= 0 /\ -v + i1 >= 0 /\ u + i1 >= 0 /\ -u + i1 >= 0 /\ a + i1 - 2 >= 0 /\ -h1 >= 0 /\ g1 - h1 >= 0 /\ -g1 - h1 >= 0 /\ d1 - h1 >= 0 /\ -d1 - h1 >= 0 /\ v - h1 >= 0 /\ -v - h1 >= 0 /\ u - h1 >= 0 /\ -u - h1 >= 0 /\ a - h1 - 2 >= 0 /\ h1 >= 0 /\ g1 + h1 >= 0 /\ -g1 + h1 >= 0 /\ d1 + h1 >= 0 /\ -d1 + h1 >= 0 /\ v + h1 >= 0 /\ -v + h1 >= 0 /\ u + h1 >= 0 /\ -u + h1 >= 0 /\ a + h1 - 2 >= 0 /\ -g1 >= 0 /\ d1 - g1 >= 0 /\ -d1 - g1 >= 0 /\ v - g1 >= 0 /\ -v - g1 >= 0 /\ u - g1 >= 0 /\ -u - g1 >= 0 /\ a - g1 - 2 >= 0 /\ g1 >= 0 /\ d1 + g1 >= 0 /\ -d1 + g1 >= 0 /\ v + g1 >= 0 /\ -v + g1 >= 0 /\ u + g1 >= 0 /\ -u + g1 >= 0 /\ a + g1 - 2 >= 0 /\ b1 - e1 >= 0 /\ -d1 >= 0 /\ v - d1 >= 0 /\ -v - d1 >= 0 /\ u - d1 >= 0 /\ -u - d1 >= 0 /\ a - d1 - 2 >= 0 /\ d1 >= 0 /\ v + d1 >= 0 /\ -v + d1 >= 0 /\ u + d1 >= 0 /\ -u + d1 >= 0 /\ a + d1 - 2 >= 0 /\ -v >= 0 /\ u - v >= 0 /\ -u - v >= 0 /\ a - v - 2 >= 0 /\ v >= 0 /\ u + v >= 0 /\ -u + v >= 0 /\ a + v - 2 >= 0 /\ -u >= 0 /\ a - u - 2 >= 0 /\ u >= 0 /\ a + u - 2 >= 0 /\ a - 2 >= 0 /\ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(a, b + 1, c, e, f, o, p, q, s, z1, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ b >= 0 /\ q >= b + 1 ] (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(z1, 2, c, e, f, o, 0, z1, s, b2, u, v, s, b1, d1, e1, g1, h1, i1, j1, m1) [ z1 >= 2 /\ s = w ] start location: f9 leaf cost: 6 By chaining the transition f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 5, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 ] with all transitions in problem 14, the following new transition is obtained: f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 6, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 ] We thus obtain the following problem: 15: T: (2, 8) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 6, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 ] (c + f + e1 + 1, 1) f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, 0, h1, w, b1, d1, e1 - 1, 0, h1, 0, h1, m1) [ -p + 1 >= 0 /\ o - p - 1 >= 0 /\ f - p - 1 >= 0 /\ j1 - p + 1 >= 0 /\ -j1 - p + 1 >= 0 /\ i1 - p + 1 >= 0 /\ -i1 - p + 1 >= 0 /\ h1 - p + 1 >= 0 /\ -h1 - p + 1 >= 0 /\ g1 - p + 1 >= 0 /\ -g1 - p + 1 >= 0 /\ d1 - p + 1 >= 0 /\ -d1 - p + 1 >= 0 /\ v - p + 1 >= 0 /\ -v - p + 1 >= 0 /\ u - p + 1 >= 0 /\ -u - p + 1 >= 0 /\ a - p - 1 >= 0 /\ p - 1 >= 0 /\ o + p - 3 >= 0 /\ f + p - 3 >= 0 /\ j1 + p - 1 >= 0 /\ -j1 + p - 1 >= 0 /\ i1 + p - 1 >= 0 /\ -i1 + p - 1 >= 0 /\ h1 + p - 1 >= 0 /\ -h1 + p - 1 >= 0 /\ g1 + p - 1 >= 0 /\ -g1 + p - 1 >= 0 /\ d1 + p - 1 >= 0 /\ -d1 + p - 1 >= 0 /\ v + p - 1 >= 0 /\ -v + p - 1 >= 0 /\ u + p - 1 >= 0 /\ -u + p - 1 >= 0 /\ a + p - 3 >= 0 /\ f - o >= 0 /\ o - 2 >= 0 /\ f + o - 4 >= 0 /\ -f + o >= 0 /\ j1 + o - 2 >= 0 /\ -j1 + o - 2 >= 0 /\ i1 + o - 2 >= 0 /\ -i1 + o - 2 >= 0 /\ h1 + o - 2 >= 0 /\ -h1 + o - 2 >= 0 /\ g1 + o - 2 >= 0 /\ -g1 + o - 2 >= 0 /\ d1 + o - 2 >= 0 /\ -d1 + o - 2 >= 0 /\ v + o - 2 >= 0 /\ -v + o - 2 >= 0 /\ u + o - 2 >= 0 /\ -u + o - 2 >= 0 /\ a + o - 4 >= 0 /\ -a + o >= 0 /\ f - 2 >= 0 /\ j1 + f - 2 >= 0 /\ -j1 + f - 2 >= 0 /\ i1 + f - 2 >= 0 /\ -i1 + f - 2 >= 0 /\ h1 + f - 2 >= 0 /\ -h1 + f - 2 >= 0 /\ g1 + f - 2 >= 0 /\ -g1 + f - 2 >= 0 /\ d1 + f - 2 >= 0 /\ -d1 + f - 2 >= 0 /\ v + f - 2 >= 0 /\ -v + f - 2 >= 0 /\ u + f - 2 >= 0 /\ -u + f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ b1 - c + 1 >= 0 /\ -e1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -j1 >= 0 /\ i1 - j1 >= 0 /\ -i1 - j1 >= 0 /\ h1 - j1 >= 0 /\ -h1 - j1 >= 0 /\ g1 - j1 >= 0 /\ -g1 - j1 >= 0 /\ d1 - j1 >= 0 /\ -d1 - j1 >= 0 /\ v - j1 >= 0 /\ -v - j1 >= 0 /\ u - j1 >= 0 /\ -u - j1 >= 0 /\ a - j1 - 2 >= 0 /\ j1 >= 0 /\ i1 + j1 >= 0 /\ -i1 + j1 >= 0 /\ h1 + j1 >= 0 /\ -h1 + j1 >= 0 /\ g1 + j1 >= 0 /\ -g1 + j1 >= 0 /\ d1 + j1 >= 0 /\ -d1 + j1 >= 0 /\ v + j1 >= 0 /\ -v + j1 >= 0 /\ u + j1 >= 0 /\ -u + j1 >= 0 /\ a + j1 - 2 >= 0 /\ -i1 >= 0 /\ h1 - i1 >= 0 /\ -h1 - i1 >= 0 /\ g1 - i1 >= 0 /\ -g1 - i1 >= 0 /\ d1 - i1 >= 0 /\ -d1 - i1 >= 0 /\ v - i1 >= 0 /\ -v - i1 >= 0 /\ u - i1 >= 0 /\ -u - i1 >= 0 /\ a - i1 - 2 >= 0 /\ i1 >= 0 /\ h1 + i1 >= 0 /\ -h1 + i1 >= 0 /\ g1 + i1 >= 0 /\ -g1 + i1 >= 0 /\ d1 + i1 >= 0 /\ -d1 + i1 >= 0 /\ v + i1 >= 0 /\ -v + i1 >= 0 /\ u + i1 >= 0 /\ -u + i1 >= 0 /\ a + i1 - 2 >= 0 /\ -h1 >= 0 /\ g1 - h1 >= 0 /\ -g1 - h1 >= 0 /\ d1 - h1 >= 0 /\ -d1 - h1 >= 0 /\ v - h1 >= 0 /\ -v - h1 >= 0 /\ u - h1 >= 0 /\ -u - h1 >= 0 /\ a - h1 - 2 >= 0 /\ h1 >= 0 /\ g1 + h1 >= 0 /\ -g1 + h1 >= 0 /\ d1 + h1 >= 0 /\ -d1 + h1 >= 0 /\ v + h1 >= 0 /\ -v + h1 >= 0 /\ u + h1 >= 0 /\ -u + h1 >= 0 /\ a + h1 - 2 >= 0 /\ -g1 >= 0 /\ d1 - g1 >= 0 /\ -d1 - g1 >= 0 /\ v - g1 >= 0 /\ -v - g1 >= 0 /\ u - g1 >= 0 /\ -u - g1 >= 0 /\ a - g1 - 2 >= 0 /\ g1 >= 0 /\ d1 + g1 >= 0 /\ -d1 + g1 >= 0 /\ v + g1 >= 0 /\ -v + g1 >= 0 /\ u + g1 >= 0 /\ -u + g1 >= 0 /\ a + g1 - 2 >= 0 /\ b1 - e1 >= 0 /\ -d1 >= 0 /\ v - d1 >= 0 /\ -v - d1 >= 0 /\ u - d1 >= 0 /\ -u - d1 >= 0 /\ a - d1 - 2 >= 0 /\ d1 >= 0 /\ v + d1 >= 0 /\ -v + d1 >= 0 /\ u + d1 >= 0 /\ -u + d1 >= 0 /\ a + d1 - 2 >= 0 /\ -v >= 0 /\ u - v >= 0 /\ -u - v >= 0 /\ a - v - 2 >= 0 /\ v >= 0 /\ u + v >= 0 /\ -u + v >= 0 /\ a + v - 2 >= 0 /\ -u >= 0 /\ a - u - 2 >= 0 /\ u >= 0 /\ a + u - 2 >= 0 /\ a - 2 >= 0 /\ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(a, b + 1, c, e, f, o, p, q, s, z1, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ b >= 0 /\ q >= b + 1 ] (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(z1, 2, c, e, f, o, 0, z1, s, b2, u, v, s, b1, d1, e1, g1, h1, i1, j1, m1) [ z1 >= 2 /\ s = w ] start location: f9 leaf cost: 6 By chaining the transition f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 6, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 ] with all transitions in problem 15, the following new transition is obtained: f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 7, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 /\ 6 >= 0 /\ e1 - 6 >= 0 ] We thus obtain the following problem: 16: T: (2, 9) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 7, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 /\ 6 >= 0 /\ e1 - 6 >= 0 ] (c + f + e1 + 1, 1) f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, 0, h1, w, b1, d1, e1 - 1, 0, h1, 0, h1, m1) [ -p + 1 >= 0 /\ o - p - 1 >= 0 /\ f - p - 1 >= 0 /\ j1 - p + 1 >= 0 /\ -j1 - p + 1 >= 0 /\ i1 - p + 1 >= 0 /\ -i1 - p + 1 >= 0 /\ h1 - p + 1 >= 0 /\ -h1 - p + 1 >= 0 /\ g1 - p + 1 >= 0 /\ -g1 - p + 1 >= 0 /\ d1 - p + 1 >= 0 /\ -d1 - p + 1 >= 0 /\ v - p + 1 >= 0 /\ -v - p + 1 >= 0 /\ u - p + 1 >= 0 /\ -u - p + 1 >= 0 /\ a - p - 1 >= 0 /\ p - 1 >= 0 /\ o + p - 3 >= 0 /\ f + p - 3 >= 0 /\ j1 + p - 1 >= 0 /\ -j1 + p - 1 >= 0 /\ i1 + p - 1 >= 0 /\ -i1 + p - 1 >= 0 /\ h1 + p - 1 >= 0 /\ -h1 + p - 1 >= 0 /\ g1 + p - 1 >= 0 /\ -g1 + p - 1 >= 0 /\ d1 + p - 1 >= 0 /\ -d1 + p - 1 >= 0 /\ v + p - 1 >= 0 /\ -v + p - 1 >= 0 /\ u + p - 1 >= 0 /\ -u + p - 1 >= 0 /\ a + p - 3 >= 0 /\ f - o >= 0 /\ o - 2 >= 0 /\ f + o - 4 >= 0 /\ -f + o >= 0 /\ j1 + o - 2 >= 0 /\ -j1 + o - 2 >= 0 /\ i1 + o - 2 >= 0 /\ -i1 + o - 2 >= 0 /\ h1 + o - 2 >= 0 /\ -h1 + o - 2 >= 0 /\ g1 + o - 2 >= 0 /\ -g1 + o - 2 >= 0 /\ d1 + o - 2 >= 0 /\ -d1 + o - 2 >= 0 /\ v + o - 2 >= 0 /\ -v + o - 2 >= 0 /\ u + o - 2 >= 0 /\ -u + o - 2 >= 0 /\ a + o - 4 >= 0 /\ -a + o >= 0 /\ f - 2 >= 0 /\ j1 + f - 2 >= 0 /\ -j1 + f - 2 >= 0 /\ i1 + f - 2 >= 0 /\ -i1 + f - 2 >= 0 /\ h1 + f - 2 >= 0 /\ -h1 + f - 2 >= 0 /\ g1 + f - 2 >= 0 /\ -g1 + f - 2 >= 0 /\ d1 + f - 2 >= 0 /\ -d1 + f - 2 >= 0 /\ v + f - 2 >= 0 /\ -v + f - 2 >= 0 /\ u + f - 2 >= 0 /\ -u + f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ b1 - c + 1 >= 0 /\ -e1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -j1 >= 0 /\ i1 - j1 >= 0 /\ -i1 - j1 >= 0 /\ h1 - j1 >= 0 /\ -h1 - j1 >= 0 /\ g1 - j1 >= 0 /\ -g1 - j1 >= 0 /\ d1 - j1 >= 0 /\ -d1 - j1 >= 0 /\ v - j1 >= 0 /\ -v - j1 >= 0 /\ u - j1 >= 0 /\ -u - j1 >= 0 /\ a - j1 - 2 >= 0 /\ j1 >= 0 /\ i1 + j1 >= 0 /\ -i1 + j1 >= 0 /\ h1 + j1 >= 0 /\ -h1 + j1 >= 0 /\ g1 + j1 >= 0 /\ -g1 + j1 >= 0 /\ d1 + j1 >= 0 /\ -d1 + j1 >= 0 /\ v + j1 >= 0 /\ -v + j1 >= 0 /\ u + j1 >= 0 /\ -u + j1 >= 0 /\ a + j1 - 2 >= 0 /\ -i1 >= 0 /\ h1 - i1 >= 0 /\ -h1 - i1 >= 0 /\ g1 - i1 >= 0 /\ -g1 - i1 >= 0 /\ d1 - i1 >= 0 /\ -d1 - i1 >= 0 /\ v - i1 >= 0 /\ -v - i1 >= 0 /\ u - i1 >= 0 /\ -u - i1 >= 0 /\ a - i1 - 2 >= 0 /\ i1 >= 0 /\ h1 + i1 >= 0 /\ -h1 + i1 >= 0 /\ g1 + i1 >= 0 /\ -g1 + i1 >= 0 /\ d1 + i1 >= 0 /\ -d1 + i1 >= 0 /\ v + i1 >= 0 /\ -v + i1 >= 0 /\ u + i1 >= 0 /\ -u + i1 >= 0 /\ a + i1 - 2 >= 0 /\ -h1 >= 0 /\ g1 - h1 >= 0 /\ -g1 - h1 >= 0 /\ d1 - h1 >= 0 /\ -d1 - h1 >= 0 /\ v - h1 >= 0 /\ -v - h1 >= 0 /\ u - h1 >= 0 /\ -u - h1 >= 0 /\ a - h1 - 2 >= 0 /\ h1 >= 0 /\ g1 + h1 >= 0 /\ -g1 + h1 >= 0 /\ d1 + h1 >= 0 /\ -d1 + h1 >= 0 /\ v + h1 >= 0 /\ -v + h1 >= 0 /\ u + h1 >= 0 /\ -u + h1 >= 0 /\ a + h1 - 2 >= 0 /\ -g1 >= 0 /\ d1 - g1 >= 0 /\ -d1 - g1 >= 0 /\ v - g1 >= 0 /\ -v - g1 >= 0 /\ u - g1 >= 0 /\ -u - g1 >= 0 /\ a - g1 - 2 >= 0 /\ g1 >= 0 /\ d1 + g1 >= 0 /\ -d1 + g1 >= 0 /\ v + g1 >= 0 /\ -v + g1 >= 0 /\ u + g1 >= 0 /\ -u + g1 >= 0 /\ a + g1 - 2 >= 0 /\ b1 - e1 >= 0 /\ -d1 >= 0 /\ v - d1 >= 0 /\ -v - d1 >= 0 /\ u - d1 >= 0 /\ -u - d1 >= 0 /\ a - d1 - 2 >= 0 /\ d1 >= 0 /\ v + d1 >= 0 /\ -v + d1 >= 0 /\ u + d1 >= 0 /\ -u + d1 >= 0 /\ a + d1 - 2 >= 0 /\ -v >= 0 /\ u - v >= 0 /\ -u - v >= 0 /\ a - v - 2 >= 0 /\ v >= 0 /\ u + v >= 0 /\ -u + v >= 0 /\ a + v - 2 >= 0 /\ -u >= 0 /\ a - u - 2 >= 0 /\ u >= 0 /\ a + u - 2 >= 0 /\ a - 2 >= 0 /\ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(a, b + 1, c, e, f, o, p, q, s, z1, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ b >= 0 /\ q >= b + 1 ] (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(z1, 2, c, e, f, o, 0, z1, s, b2, u, v, s, b1, d1, e1, g1, h1, i1, j1, m1) [ z1 >= 2 /\ s = w ] start location: f9 leaf cost: 6 By chaining the transition f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 7, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 /\ 6 >= 0 /\ e1 - 6 >= 0 ] with all transitions in problem 16, the following new transition is obtained: f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 8, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 /\ 6 >= 0 /\ e1 - 6 >= 0 /\ 7 >= 0 /\ e1 - 7 >= 0 ] We thus obtain the following problem: 17: T: (2, 10) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 8, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 /\ 6 >= 0 /\ e1 - 6 >= 0 /\ 7 >= 0 /\ e1 - 7 >= 0 ] (c + f + e1 + 1, 1) f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, 0, h1, w, b1, d1, e1 - 1, 0, h1, 0, h1, m1) [ -p + 1 >= 0 /\ o - p - 1 >= 0 /\ f - p - 1 >= 0 /\ j1 - p + 1 >= 0 /\ -j1 - p + 1 >= 0 /\ i1 - p + 1 >= 0 /\ -i1 - p + 1 >= 0 /\ h1 - p + 1 >= 0 /\ -h1 - p + 1 >= 0 /\ g1 - p + 1 >= 0 /\ -g1 - p + 1 >= 0 /\ d1 - p + 1 >= 0 /\ -d1 - p + 1 >= 0 /\ v - p + 1 >= 0 /\ -v - p + 1 >= 0 /\ u - p + 1 >= 0 /\ -u - p + 1 >= 0 /\ a - p - 1 >= 0 /\ p - 1 >= 0 /\ o + p - 3 >= 0 /\ f + p - 3 >= 0 /\ j1 + p - 1 >= 0 /\ -j1 + p - 1 >= 0 /\ i1 + p - 1 >= 0 /\ -i1 + p - 1 >= 0 /\ h1 + p - 1 >= 0 /\ -h1 + p - 1 >= 0 /\ g1 + p - 1 >= 0 /\ -g1 + p - 1 >= 0 /\ d1 + p - 1 >= 0 /\ -d1 + p - 1 >= 0 /\ v + p - 1 >= 0 /\ -v + p - 1 >= 0 /\ u + p - 1 >= 0 /\ -u + p - 1 >= 0 /\ a + p - 3 >= 0 /\ f - o >= 0 /\ o - 2 >= 0 /\ f + o - 4 >= 0 /\ -f + o >= 0 /\ j1 + o - 2 >= 0 /\ -j1 + o - 2 >= 0 /\ i1 + o - 2 >= 0 /\ -i1 + o - 2 >= 0 /\ h1 + o - 2 >= 0 /\ -h1 + o - 2 >= 0 /\ g1 + o - 2 >= 0 /\ -g1 + o - 2 >= 0 /\ d1 + o - 2 >= 0 /\ -d1 + o - 2 >= 0 /\ v + o - 2 >= 0 /\ -v + o - 2 >= 0 /\ u + o - 2 >= 0 /\ -u + o - 2 >= 0 /\ a + o - 4 >= 0 /\ -a + o >= 0 /\ f - 2 >= 0 /\ j1 + f - 2 >= 0 /\ -j1 + f - 2 >= 0 /\ i1 + f - 2 >= 0 /\ -i1 + f - 2 >= 0 /\ h1 + f - 2 >= 0 /\ -h1 + f - 2 >= 0 /\ g1 + f - 2 >= 0 /\ -g1 + f - 2 >= 0 /\ d1 + f - 2 >= 0 /\ -d1 + f - 2 >= 0 /\ v + f - 2 >= 0 /\ -v + f - 2 >= 0 /\ u + f - 2 >= 0 /\ -u + f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ b1 - c + 1 >= 0 /\ -e1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -j1 >= 0 /\ i1 - j1 >= 0 /\ -i1 - j1 >= 0 /\ h1 - j1 >= 0 /\ -h1 - j1 >= 0 /\ g1 - j1 >= 0 /\ -g1 - j1 >= 0 /\ d1 - j1 >= 0 /\ -d1 - j1 >= 0 /\ v - j1 >= 0 /\ -v - j1 >= 0 /\ u - j1 >= 0 /\ -u - j1 >= 0 /\ a - j1 - 2 >= 0 /\ j1 >= 0 /\ i1 + j1 >= 0 /\ -i1 + j1 >= 0 /\ h1 + j1 >= 0 /\ -h1 + j1 >= 0 /\ g1 + j1 >= 0 /\ -g1 + j1 >= 0 /\ d1 + j1 >= 0 /\ -d1 + j1 >= 0 /\ v + j1 >= 0 /\ -v + j1 >= 0 /\ u + j1 >= 0 /\ -u + j1 >= 0 /\ a + j1 - 2 >= 0 /\ -i1 >= 0 /\ h1 - i1 >= 0 /\ -h1 - i1 >= 0 /\ g1 - i1 >= 0 /\ -g1 - i1 >= 0 /\ d1 - i1 >= 0 /\ -d1 - i1 >= 0 /\ v - i1 >= 0 /\ -v - i1 >= 0 /\ u - i1 >= 0 /\ -u - i1 >= 0 /\ a - i1 - 2 >= 0 /\ i1 >= 0 /\ h1 + i1 >= 0 /\ -h1 + i1 >= 0 /\ g1 + i1 >= 0 /\ -g1 + i1 >= 0 /\ d1 + i1 >= 0 /\ -d1 + i1 >= 0 /\ v + i1 >= 0 /\ -v + i1 >= 0 /\ u + i1 >= 0 /\ -u + i1 >= 0 /\ a + i1 - 2 >= 0 /\ -h1 >= 0 /\ g1 - h1 >= 0 /\ -g1 - h1 >= 0 /\ d1 - h1 >= 0 /\ -d1 - h1 >= 0 /\ v - h1 >= 0 /\ -v - h1 >= 0 /\ u - h1 >= 0 /\ -u - h1 >= 0 /\ a - h1 - 2 >= 0 /\ h1 >= 0 /\ g1 + h1 >= 0 /\ -g1 + h1 >= 0 /\ d1 + h1 >= 0 /\ -d1 + h1 >= 0 /\ v + h1 >= 0 /\ -v + h1 >= 0 /\ u + h1 >= 0 /\ -u + h1 >= 0 /\ a + h1 - 2 >= 0 /\ -g1 >= 0 /\ d1 - g1 >= 0 /\ -d1 - g1 >= 0 /\ v - g1 >= 0 /\ -v - g1 >= 0 /\ u - g1 >= 0 /\ -u - g1 >= 0 /\ a - g1 - 2 >= 0 /\ g1 >= 0 /\ d1 + g1 >= 0 /\ -d1 + g1 >= 0 /\ v + g1 >= 0 /\ -v + g1 >= 0 /\ u + g1 >= 0 /\ -u + g1 >= 0 /\ a + g1 - 2 >= 0 /\ b1 - e1 >= 0 /\ -d1 >= 0 /\ v - d1 >= 0 /\ -v - d1 >= 0 /\ u - d1 >= 0 /\ -u - d1 >= 0 /\ a - d1 - 2 >= 0 /\ d1 >= 0 /\ v + d1 >= 0 /\ -v + d1 >= 0 /\ u + d1 >= 0 /\ -u + d1 >= 0 /\ a + d1 - 2 >= 0 /\ -v >= 0 /\ u - v >= 0 /\ -u - v >= 0 /\ a - v - 2 >= 0 /\ v >= 0 /\ u + v >= 0 /\ -u + v >= 0 /\ a + v - 2 >= 0 /\ -u >= 0 /\ a - u - 2 >= 0 /\ u >= 0 /\ a + u - 2 >= 0 /\ a - 2 >= 0 /\ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(a, b + 1, c, e, f, o, p, q, s, z1, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ b >= 0 /\ q >= b + 1 ] (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(z1, 2, c, e, f, o, 0, z1, s, b2, u, v, s, b1, d1, e1, g1, h1, i1, j1, m1) [ z1 >= 2 /\ s = w ] start location: f9 leaf cost: 6 By chaining the transition f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 8, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 /\ 6 >= 0 /\ e1 - 6 >= 0 /\ 7 >= 0 /\ e1 - 7 >= 0 ] with all transitions in problem 17, the following new transition is obtained: f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 9, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 /\ 6 >= 0 /\ e1 - 6 >= 0 /\ 7 >= 0 /\ e1 - 7 >= 0 /\ 8 >= 0 /\ e1 - 8 >= 0 ] We thus obtain the following problem: 18: T: (2, 11) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 9, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 /\ 6 >= 0 /\ e1 - 6 >= 0 /\ 7 >= 0 /\ e1 - 7 >= 0 /\ 8 >= 0 /\ e1 - 8 >= 0 ] (c + f + e1 + 1, 1) f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, 0, h1, w, b1, d1, e1 - 1, 0, h1, 0, h1, m1) [ -p + 1 >= 0 /\ o - p - 1 >= 0 /\ f - p - 1 >= 0 /\ j1 - p + 1 >= 0 /\ -j1 - p + 1 >= 0 /\ i1 - p + 1 >= 0 /\ -i1 - p + 1 >= 0 /\ h1 - p + 1 >= 0 /\ -h1 - p + 1 >= 0 /\ g1 - p + 1 >= 0 /\ -g1 - p + 1 >= 0 /\ d1 - p + 1 >= 0 /\ -d1 - p + 1 >= 0 /\ v - p + 1 >= 0 /\ -v - p + 1 >= 0 /\ u - p + 1 >= 0 /\ -u - p + 1 >= 0 /\ a - p - 1 >= 0 /\ p - 1 >= 0 /\ o + p - 3 >= 0 /\ f + p - 3 >= 0 /\ j1 + p - 1 >= 0 /\ -j1 + p - 1 >= 0 /\ i1 + p - 1 >= 0 /\ -i1 + p - 1 >= 0 /\ h1 + p - 1 >= 0 /\ -h1 + p - 1 >= 0 /\ g1 + p - 1 >= 0 /\ -g1 + p - 1 >= 0 /\ d1 + p - 1 >= 0 /\ -d1 + p - 1 >= 0 /\ v + p - 1 >= 0 /\ -v + p - 1 >= 0 /\ u + p - 1 >= 0 /\ -u + p - 1 >= 0 /\ a + p - 3 >= 0 /\ f - o >= 0 /\ o - 2 >= 0 /\ f + o - 4 >= 0 /\ -f + o >= 0 /\ j1 + o - 2 >= 0 /\ -j1 + o - 2 >= 0 /\ i1 + o - 2 >= 0 /\ -i1 + o - 2 >= 0 /\ h1 + o - 2 >= 0 /\ -h1 + o - 2 >= 0 /\ g1 + o - 2 >= 0 /\ -g1 + o - 2 >= 0 /\ d1 + o - 2 >= 0 /\ -d1 + o - 2 >= 0 /\ v + o - 2 >= 0 /\ -v + o - 2 >= 0 /\ u + o - 2 >= 0 /\ -u + o - 2 >= 0 /\ a + o - 4 >= 0 /\ -a + o >= 0 /\ f - 2 >= 0 /\ j1 + f - 2 >= 0 /\ -j1 + f - 2 >= 0 /\ i1 + f - 2 >= 0 /\ -i1 + f - 2 >= 0 /\ h1 + f - 2 >= 0 /\ -h1 + f - 2 >= 0 /\ g1 + f - 2 >= 0 /\ -g1 + f - 2 >= 0 /\ d1 + f - 2 >= 0 /\ -d1 + f - 2 >= 0 /\ v + f - 2 >= 0 /\ -v + f - 2 >= 0 /\ u + f - 2 >= 0 /\ -u + f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ b1 - c + 1 >= 0 /\ -e1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -j1 >= 0 /\ i1 - j1 >= 0 /\ -i1 - j1 >= 0 /\ h1 - j1 >= 0 /\ -h1 - j1 >= 0 /\ g1 - j1 >= 0 /\ -g1 - j1 >= 0 /\ d1 - j1 >= 0 /\ -d1 - j1 >= 0 /\ v - j1 >= 0 /\ -v - j1 >= 0 /\ u - j1 >= 0 /\ -u - j1 >= 0 /\ a - j1 - 2 >= 0 /\ j1 >= 0 /\ i1 + j1 >= 0 /\ -i1 + j1 >= 0 /\ h1 + j1 >= 0 /\ -h1 + j1 >= 0 /\ g1 + j1 >= 0 /\ -g1 + j1 >= 0 /\ d1 + j1 >= 0 /\ -d1 + j1 >= 0 /\ v + j1 >= 0 /\ -v + j1 >= 0 /\ u + j1 >= 0 /\ -u + j1 >= 0 /\ a + j1 - 2 >= 0 /\ -i1 >= 0 /\ h1 - i1 >= 0 /\ -h1 - i1 >= 0 /\ g1 - i1 >= 0 /\ -g1 - i1 >= 0 /\ d1 - i1 >= 0 /\ -d1 - i1 >= 0 /\ v - i1 >= 0 /\ -v - i1 >= 0 /\ u - i1 >= 0 /\ -u - i1 >= 0 /\ a - i1 - 2 >= 0 /\ i1 >= 0 /\ h1 + i1 >= 0 /\ -h1 + i1 >= 0 /\ g1 + i1 >= 0 /\ -g1 + i1 >= 0 /\ d1 + i1 >= 0 /\ -d1 + i1 >= 0 /\ v + i1 >= 0 /\ -v + i1 >= 0 /\ u + i1 >= 0 /\ -u + i1 >= 0 /\ a + i1 - 2 >= 0 /\ -h1 >= 0 /\ g1 - h1 >= 0 /\ -g1 - h1 >= 0 /\ d1 - h1 >= 0 /\ -d1 - h1 >= 0 /\ v - h1 >= 0 /\ -v - h1 >= 0 /\ u - h1 >= 0 /\ -u - h1 >= 0 /\ a - h1 - 2 >= 0 /\ h1 >= 0 /\ g1 + h1 >= 0 /\ -g1 + h1 >= 0 /\ d1 + h1 >= 0 /\ -d1 + h1 >= 0 /\ v + h1 >= 0 /\ -v + h1 >= 0 /\ u + h1 >= 0 /\ -u + h1 >= 0 /\ a + h1 - 2 >= 0 /\ -g1 >= 0 /\ d1 - g1 >= 0 /\ -d1 - g1 >= 0 /\ v - g1 >= 0 /\ -v - g1 >= 0 /\ u - g1 >= 0 /\ -u - g1 >= 0 /\ a - g1 - 2 >= 0 /\ g1 >= 0 /\ d1 + g1 >= 0 /\ -d1 + g1 >= 0 /\ v + g1 >= 0 /\ -v + g1 >= 0 /\ u + g1 >= 0 /\ -u + g1 >= 0 /\ a + g1 - 2 >= 0 /\ b1 - e1 >= 0 /\ -d1 >= 0 /\ v - d1 >= 0 /\ -v - d1 >= 0 /\ u - d1 >= 0 /\ -u - d1 >= 0 /\ a - d1 - 2 >= 0 /\ d1 >= 0 /\ v + d1 >= 0 /\ -v + d1 >= 0 /\ u + d1 >= 0 /\ -u + d1 >= 0 /\ a + d1 - 2 >= 0 /\ -v >= 0 /\ u - v >= 0 /\ -u - v >= 0 /\ a - v - 2 >= 0 /\ v >= 0 /\ u + v >= 0 /\ -u + v >= 0 /\ a + v - 2 >= 0 /\ -u >= 0 /\ a - u - 2 >= 0 /\ u >= 0 /\ a + u - 2 >= 0 /\ a - 2 >= 0 /\ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(a, b + 1, c, e, f, o, p, q, s, z1, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ b >= 0 /\ q >= b + 1 ] (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(z1, 2, c, e, f, o, 0, z1, s, b2, u, v, s, b1, d1, e1, g1, h1, i1, j1, m1) [ z1 >= 2 /\ s = w ] start location: f9 leaf cost: 6 By chaining the transition f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 9, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 /\ 6 >= 0 /\ e1 - 6 >= 0 /\ 7 >= 0 /\ e1 - 7 >= 0 /\ 8 >= 0 /\ e1 - 8 >= 0 ] with all transitions in problem 18, the following new transition is obtained: f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 10, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 /\ 6 >= 0 /\ e1 - 6 >= 0 /\ 7 >= 0 /\ e1 - 7 >= 0 /\ 8 >= 0 /\ e1 - 8 >= 0 /\ 9 >= 0 /\ e1 - 9 >= 0 ] We thus obtain the following problem: 19: T: (2, 12) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 10, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 /\ 6 >= 0 /\ e1 - 6 >= 0 /\ 7 >= 0 /\ e1 - 7 >= 0 /\ 8 >= 0 /\ e1 - 8 >= 0 /\ 9 >= 0 /\ e1 - 9 >= 0 ] (c + f + e1 + 1, 1) f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, 0, h1, w, b1, d1, e1 - 1, 0, h1, 0, h1, m1) [ -p + 1 >= 0 /\ o - p - 1 >= 0 /\ f - p - 1 >= 0 /\ j1 - p + 1 >= 0 /\ -j1 - p + 1 >= 0 /\ i1 - p + 1 >= 0 /\ -i1 - p + 1 >= 0 /\ h1 - p + 1 >= 0 /\ -h1 - p + 1 >= 0 /\ g1 - p + 1 >= 0 /\ -g1 - p + 1 >= 0 /\ d1 - p + 1 >= 0 /\ -d1 - p + 1 >= 0 /\ v - p + 1 >= 0 /\ -v - p + 1 >= 0 /\ u - p + 1 >= 0 /\ -u - p + 1 >= 0 /\ a - p - 1 >= 0 /\ p - 1 >= 0 /\ o + p - 3 >= 0 /\ f + p - 3 >= 0 /\ j1 + p - 1 >= 0 /\ -j1 + p - 1 >= 0 /\ i1 + p - 1 >= 0 /\ -i1 + p - 1 >= 0 /\ h1 + p - 1 >= 0 /\ -h1 + p - 1 >= 0 /\ g1 + p - 1 >= 0 /\ -g1 + p - 1 >= 0 /\ d1 + p - 1 >= 0 /\ -d1 + p - 1 >= 0 /\ v + p - 1 >= 0 /\ -v + p - 1 >= 0 /\ u + p - 1 >= 0 /\ -u + p - 1 >= 0 /\ a + p - 3 >= 0 /\ f - o >= 0 /\ o - 2 >= 0 /\ f + o - 4 >= 0 /\ -f + o >= 0 /\ j1 + o - 2 >= 0 /\ -j1 + o - 2 >= 0 /\ i1 + o - 2 >= 0 /\ -i1 + o - 2 >= 0 /\ h1 + o - 2 >= 0 /\ -h1 + o - 2 >= 0 /\ g1 + o - 2 >= 0 /\ -g1 + o - 2 >= 0 /\ d1 + o - 2 >= 0 /\ -d1 + o - 2 >= 0 /\ v + o - 2 >= 0 /\ -v + o - 2 >= 0 /\ u + o - 2 >= 0 /\ -u + o - 2 >= 0 /\ a + o - 4 >= 0 /\ -a + o >= 0 /\ f - 2 >= 0 /\ j1 + f - 2 >= 0 /\ -j1 + f - 2 >= 0 /\ i1 + f - 2 >= 0 /\ -i1 + f - 2 >= 0 /\ h1 + f - 2 >= 0 /\ -h1 + f - 2 >= 0 /\ g1 + f - 2 >= 0 /\ -g1 + f - 2 >= 0 /\ d1 + f - 2 >= 0 /\ -d1 + f - 2 >= 0 /\ v + f - 2 >= 0 /\ -v + f - 2 >= 0 /\ u + f - 2 >= 0 /\ -u + f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ b1 - c + 1 >= 0 /\ -e1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -j1 >= 0 /\ i1 - j1 >= 0 /\ -i1 - j1 >= 0 /\ h1 - j1 >= 0 /\ -h1 - j1 >= 0 /\ g1 - j1 >= 0 /\ -g1 - j1 >= 0 /\ d1 - j1 >= 0 /\ -d1 - j1 >= 0 /\ v - j1 >= 0 /\ -v - j1 >= 0 /\ u - j1 >= 0 /\ -u - j1 >= 0 /\ a - j1 - 2 >= 0 /\ j1 >= 0 /\ i1 + j1 >= 0 /\ -i1 + j1 >= 0 /\ h1 + j1 >= 0 /\ -h1 + j1 >= 0 /\ g1 + j1 >= 0 /\ -g1 + j1 >= 0 /\ d1 + j1 >= 0 /\ -d1 + j1 >= 0 /\ v + j1 >= 0 /\ -v + j1 >= 0 /\ u + j1 >= 0 /\ -u + j1 >= 0 /\ a + j1 - 2 >= 0 /\ -i1 >= 0 /\ h1 - i1 >= 0 /\ -h1 - i1 >= 0 /\ g1 - i1 >= 0 /\ -g1 - i1 >= 0 /\ d1 - i1 >= 0 /\ -d1 - i1 >= 0 /\ v - i1 >= 0 /\ -v - i1 >= 0 /\ u - i1 >= 0 /\ -u - i1 >= 0 /\ a - i1 - 2 >= 0 /\ i1 >= 0 /\ h1 + i1 >= 0 /\ -h1 + i1 >= 0 /\ g1 + i1 >= 0 /\ -g1 + i1 >= 0 /\ d1 + i1 >= 0 /\ -d1 + i1 >= 0 /\ v + i1 >= 0 /\ -v + i1 >= 0 /\ u + i1 >= 0 /\ -u + i1 >= 0 /\ a + i1 - 2 >= 0 /\ -h1 >= 0 /\ g1 - h1 >= 0 /\ -g1 - h1 >= 0 /\ d1 - h1 >= 0 /\ -d1 - h1 >= 0 /\ v - h1 >= 0 /\ -v - h1 >= 0 /\ u - h1 >= 0 /\ -u - h1 >= 0 /\ a - h1 - 2 >= 0 /\ h1 >= 0 /\ g1 + h1 >= 0 /\ -g1 + h1 >= 0 /\ d1 + h1 >= 0 /\ -d1 + h1 >= 0 /\ v + h1 >= 0 /\ -v + h1 >= 0 /\ u + h1 >= 0 /\ -u + h1 >= 0 /\ a + h1 - 2 >= 0 /\ -g1 >= 0 /\ d1 - g1 >= 0 /\ -d1 - g1 >= 0 /\ v - g1 >= 0 /\ -v - g1 >= 0 /\ u - g1 >= 0 /\ -u - g1 >= 0 /\ a - g1 - 2 >= 0 /\ g1 >= 0 /\ d1 + g1 >= 0 /\ -d1 + g1 >= 0 /\ v + g1 >= 0 /\ -v + g1 >= 0 /\ u + g1 >= 0 /\ -u + g1 >= 0 /\ a + g1 - 2 >= 0 /\ b1 - e1 >= 0 /\ -d1 >= 0 /\ v - d1 >= 0 /\ -v - d1 >= 0 /\ u - d1 >= 0 /\ -u - d1 >= 0 /\ a - d1 - 2 >= 0 /\ d1 >= 0 /\ v + d1 >= 0 /\ -v + d1 >= 0 /\ u + d1 >= 0 /\ -u + d1 >= 0 /\ a + d1 - 2 >= 0 /\ -v >= 0 /\ u - v >= 0 /\ -u - v >= 0 /\ a - v - 2 >= 0 /\ v >= 0 /\ u + v >= 0 /\ -u + v >= 0 /\ a + v - 2 >= 0 /\ -u >= 0 /\ a - u - 2 >= 0 /\ u >= 0 /\ a + u - 2 >= 0 /\ a - 2 >= 0 /\ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(a, b + 1, c, e, f, o, p, q, s, z1, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ b >= 0 /\ q >= b + 1 ] (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(z1, 2, c, e, f, o, 0, z1, s, b2, u, v, s, b1, d1, e1, g1, h1, i1, j1, m1) [ z1 >= 2 /\ s = w ] start location: f9 leaf cost: 6 By chaining the transition f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 10, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 /\ 6 >= 0 /\ e1 - 6 >= 0 /\ 7 >= 0 /\ e1 - 7 >= 0 /\ 8 >= 0 /\ e1 - 8 >= 0 /\ 9 >= 0 /\ e1 - 9 >= 0 ] with all transitions in problem 19, the following new transition is obtained: f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 11, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 /\ 6 >= 0 /\ e1 - 6 >= 0 /\ 7 >= 0 /\ e1 - 7 >= 0 /\ 8 >= 0 /\ e1 - 8 >= 0 /\ 9 >= 0 /\ e1 - 9 >= 0 /\ 10 >= 0 /\ e1 - 10 >= 0 ] We thus obtain the following problem: 20: T: (2, 13) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 11, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 /\ 6 >= 0 /\ e1 - 6 >= 0 /\ 7 >= 0 /\ e1 - 7 >= 0 /\ 8 >= 0 /\ e1 - 8 >= 0 /\ 9 >= 0 /\ e1 - 9 >= 0 /\ 10 >= 0 /\ e1 - 10 >= 0 ] (c + f + e1 + 1, 1) f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, 0, h1, w, b1, d1, e1 - 1, 0, h1, 0, h1, m1) [ -p + 1 >= 0 /\ o - p - 1 >= 0 /\ f - p - 1 >= 0 /\ j1 - p + 1 >= 0 /\ -j1 - p + 1 >= 0 /\ i1 - p + 1 >= 0 /\ -i1 - p + 1 >= 0 /\ h1 - p + 1 >= 0 /\ -h1 - p + 1 >= 0 /\ g1 - p + 1 >= 0 /\ -g1 - p + 1 >= 0 /\ d1 - p + 1 >= 0 /\ -d1 - p + 1 >= 0 /\ v - p + 1 >= 0 /\ -v - p + 1 >= 0 /\ u - p + 1 >= 0 /\ -u - p + 1 >= 0 /\ a - p - 1 >= 0 /\ p - 1 >= 0 /\ o + p - 3 >= 0 /\ f + p - 3 >= 0 /\ j1 + p - 1 >= 0 /\ -j1 + p - 1 >= 0 /\ i1 + p - 1 >= 0 /\ -i1 + p - 1 >= 0 /\ h1 + p - 1 >= 0 /\ -h1 + p - 1 >= 0 /\ g1 + p - 1 >= 0 /\ -g1 + p - 1 >= 0 /\ d1 + p - 1 >= 0 /\ -d1 + p - 1 >= 0 /\ v + p - 1 >= 0 /\ -v + p - 1 >= 0 /\ u + p - 1 >= 0 /\ -u + p - 1 >= 0 /\ a + p - 3 >= 0 /\ f - o >= 0 /\ o - 2 >= 0 /\ f + o - 4 >= 0 /\ -f + o >= 0 /\ j1 + o - 2 >= 0 /\ -j1 + o - 2 >= 0 /\ i1 + o - 2 >= 0 /\ -i1 + o - 2 >= 0 /\ h1 + o - 2 >= 0 /\ -h1 + o - 2 >= 0 /\ g1 + o - 2 >= 0 /\ -g1 + o - 2 >= 0 /\ d1 + o - 2 >= 0 /\ -d1 + o - 2 >= 0 /\ v + o - 2 >= 0 /\ -v + o - 2 >= 0 /\ u + o - 2 >= 0 /\ -u + o - 2 >= 0 /\ a + o - 4 >= 0 /\ -a + o >= 0 /\ f - 2 >= 0 /\ j1 + f - 2 >= 0 /\ -j1 + f - 2 >= 0 /\ i1 + f - 2 >= 0 /\ -i1 + f - 2 >= 0 /\ h1 + f - 2 >= 0 /\ -h1 + f - 2 >= 0 /\ g1 + f - 2 >= 0 /\ -g1 + f - 2 >= 0 /\ d1 + f - 2 >= 0 /\ -d1 + f - 2 >= 0 /\ v + f - 2 >= 0 /\ -v + f - 2 >= 0 /\ u + f - 2 >= 0 /\ -u + f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ b1 - c + 1 >= 0 /\ -e1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -j1 >= 0 /\ i1 - j1 >= 0 /\ -i1 - j1 >= 0 /\ h1 - j1 >= 0 /\ -h1 - j1 >= 0 /\ g1 - j1 >= 0 /\ -g1 - j1 >= 0 /\ d1 - j1 >= 0 /\ -d1 - j1 >= 0 /\ v - j1 >= 0 /\ -v - j1 >= 0 /\ u - j1 >= 0 /\ -u - j1 >= 0 /\ a - j1 - 2 >= 0 /\ j1 >= 0 /\ i1 + j1 >= 0 /\ -i1 + j1 >= 0 /\ h1 + j1 >= 0 /\ -h1 + j1 >= 0 /\ g1 + j1 >= 0 /\ -g1 + j1 >= 0 /\ d1 + j1 >= 0 /\ -d1 + j1 >= 0 /\ v + j1 >= 0 /\ -v + j1 >= 0 /\ u + j1 >= 0 /\ -u + j1 >= 0 /\ a + j1 - 2 >= 0 /\ -i1 >= 0 /\ h1 - i1 >= 0 /\ -h1 - i1 >= 0 /\ g1 - i1 >= 0 /\ -g1 - i1 >= 0 /\ d1 - i1 >= 0 /\ -d1 - i1 >= 0 /\ v - i1 >= 0 /\ -v - i1 >= 0 /\ u - i1 >= 0 /\ -u - i1 >= 0 /\ a - i1 - 2 >= 0 /\ i1 >= 0 /\ h1 + i1 >= 0 /\ -h1 + i1 >= 0 /\ g1 + i1 >= 0 /\ -g1 + i1 >= 0 /\ d1 + i1 >= 0 /\ -d1 + i1 >= 0 /\ v + i1 >= 0 /\ -v + i1 >= 0 /\ u + i1 >= 0 /\ -u + i1 >= 0 /\ a + i1 - 2 >= 0 /\ -h1 >= 0 /\ g1 - h1 >= 0 /\ -g1 - h1 >= 0 /\ d1 - h1 >= 0 /\ -d1 - h1 >= 0 /\ v - h1 >= 0 /\ -v - h1 >= 0 /\ u - h1 >= 0 /\ -u - h1 >= 0 /\ a - h1 - 2 >= 0 /\ h1 >= 0 /\ g1 + h1 >= 0 /\ -g1 + h1 >= 0 /\ d1 + h1 >= 0 /\ -d1 + h1 >= 0 /\ v + h1 >= 0 /\ -v + h1 >= 0 /\ u + h1 >= 0 /\ -u + h1 >= 0 /\ a + h1 - 2 >= 0 /\ -g1 >= 0 /\ d1 - g1 >= 0 /\ -d1 - g1 >= 0 /\ v - g1 >= 0 /\ -v - g1 >= 0 /\ u - g1 >= 0 /\ -u - g1 >= 0 /\ a - g1 - 2 >= 0 /\ g1 >= 0 /\ d1 + g1 >= 0 /\ -d1 + g1 >= 0 /\ v + g1 >= 0 /\ -v + g1 >= 0 /\ u + g1 >= 0 /\ -u + g1 >= 0 /\ a + g1 - 2 >= 0 /\ b1 - e1 >= 0 /\ -d1 >= 0 /\ v - d1 >= 0 /\ -v - d1 >= 0 /\ u - d1 >= 0 /\ -u - d1 >= 0 /\ a - d1 - 2 >= 0 /\ d1 >= 0 /\ v + d1 >= 0 /\ -v + d1 >= 0 /\ u + d1 >= 0 /\ -u + d1 >= 0 /\ a + d1 - 2 >= 0 /\ -v >= 0 /\ u - v >= 0 /\ -u - v >= 0 /\ a - v - 2 >= 0 /\ v >= 0 /\ u + v >= 0 /\ -u + v >= 0 /\ a + v - 2 >= 0 /\ -u >= 0 /\ a - u - 2 >= 0 /\ u >= 0 /\ a + u - 2 >= 0 /\ a - 2 >= 0 /\ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(a, b + 1, c, e, f, o, p, q, s, z1, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ b >= 0 /\ q >= b + 1 ] (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(z1, 2, c, e, f, o, 0, z1, s, b2, u, v, s, b1, d1, e1, g1, h1, i1, j1, m1) [ z1 >= 2 /\ s = w ] start location: f9 leaf cost: 6 By chaining the transition f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 11, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 /\ 6 >= 0 /\ e1 - 6 >= 0 /\ 7 >= 0 /\ e1 - 7 >= 0 /\ 8 >= 0 /\ e1 - 8 >= 0 /\ 9 >= 0 /\ e1 - 9 >= 0 /\ 10 >= 0 /\ e1 - 10 >= 0 ] with all transitions in problem 20, the following new transition is obtained: f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 12, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 /\ 6 >= 0 /\ e1 - 6 >= 0 /\ 7 >= 0 /\ e1 - 7 >= 0 /\ 8 >= 0 /\ e1 - 8 >= 0 /\ 9 >= 0 /\ e1 - 9 >= 0 /\ 10 >= 0 /\ e1 - 10 >= 0 /\ 11 >= 0 /\ e1 - 11 >= 0 ] We thus obtain the following problem: 21: T: (2, 14) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 12, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 /\ 6 >= 0 /\ e1 - 6 >= 0 /\ 7 >= 0 /\ e1 - 7 >= 0 /\ 8 >= 0 /\ e1 - 8 >= 0 /\ 9 >= 0 /\ e1 - 9 >= 0 /\ 10 >= 0 /\ e1 - 10 >= 0 /\ 11 >= 0 /\ e1 - 11 >= 0 ] (c + f + e1 + 1, 1) f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, 0, h1, w, b1, d1, e1 - 1, 0, h1, 0, h1, m1) [ -p + 1 >= 0 /\ o - p - 1 >= 0 /\ f - p - 1 >= 0 /\ j1 - p + 1 >= 0 /\ -j1 - p + 1 >= 0 /\ i1 - p + 1 >= 0 /\ -i1 - p + 1 >= 0 /\ h1 - p + 1 >= 0 /\ -h1 - p + 1 >= 0 /\ g1 - p + 1 >= 0 /\ -g1 - p + 1 >= 0 /\ d1 - p + 1 >= 0 /\ -d1 - p + 1 >= 0 /\ v - p + 1 >= 0 /\ -v - p + 1 >= 0 /\ u - p + 1 >= 0 /\ -u - p + 1 >= 0 /\ a - p - 1 >= 0 /\ p - 1 >= 0 /\ o + p - 3 >= 0 /\ f + p - 3 >= 0 /\ j1 + p - 1 >= 0 /\ -j1 + p - 1 >= 0 /\ i1 + p - 1 >= 0 /\ -i1 + p - 1 >= 0 /\ h1 + p - 1 >= 0 /\ -h1 + p - 1 >= 0 /\ g1 + p - 1 >= 0 /\ -g1 + p - 1 >= 0 /\ d1 + p - 1 >= 0 /\ -d1 + p - 1 >= 0 /\ v + p - 1 >= 0 /\ -v + p - 1 >= 0 /\ u + p - 1 >= 0 /\ -u + p - 1 >= 0 /\ a + p - 3 >= 0 /\ f - o >= 0 /\ o - 2 >= 0 /\ f + o - 4 >= 0 /\ -f + o >= 0 /\ j1 + o - 2 >= 0 /\ -j1 + o - 2 >= 0 /\ i1 + o - 2 >= 0 /\ -i1 + o - 2 >= 0 /\ h1 + o - 2 >= 0 /\ -h1 + o - 2 >= 0 /\ g1 + o - 2 >= 0 /\ -g1 + o - 2 >= 0 /\ d1 + o - 2 >= 0 /\ -d1 + o - 2 >= 0 /\ v + o - 2 >= 0 /\ -v + o - 2 >= 0 /\ u + o - 2 >= 0 /\ -u + o - 2 >= 0 /\ a + o - 4 >= 0 /\ -a + o >= 0 /\ f - 2 >= 0 /\ j1 + f - 2 >= 0 /\ -j1 + f - 2 >= 0 /\ i1 + f - 2 >= 0 /\ -i1 + f - 2 >= 0 /\ h1 + f - 2 >= 0 /\ -h1 + f - 2 >= 0 /\ g1 + f - 2 >= 0 /\ -g1 + f - 2 >= 0 /\ d1 + f - 2 >= 0 /\ -d1 + f - 2 >= 0 /\ v + f - 2 >= 0 /\ -v + f - 2 >= 0 /\ u + f - 2 >= 0 /\ -u + f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ b1 - c + 1 >= 0 /\ -e1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -j1 >= 0 /\ i1 - j1 >= 0 /\ -i1 - j1 >= 0 /\ h1 - j1 >= 0 /\ -h1 - j1 >= 0 /\ g1 - j1 >= 0 /\ -g1 - j1 >= 0 /\ d1 - j1 >= 0 /\ -d1 - j1 >= 0 /\ v - j1 >= 0 /\ -v - j1 >= 0 /\ u - j1 >= 0 /\ -u - j1 >= 0 /\ a - j1 - 2 >= 0 /\ j1 >= 0 /\ i1 + j1 >= 0 /\ -i1 + j1 >= 0 /\ h1 + j1 >= 0 /\ -h1 + j1 >= 0 /\ g1 + j1 >= 0 /\ -g1 + j1 >= 0 /\ d1 + j1 >= 0 /\ -d1 + j1 >= 0 /\ v + j1 >= 0 /\ -v + j1 >= 0 /\ u + j1 >= 0 /\ -u + j1 >= 0 /\ a + j1 - 2 >= 0 /\ -i1 >= 0 /\ h1 - i1 >= 0 /\ -h1 - i1 >= 0 /\ g1 - i1 >= 0 /\ -g1 - i1 >= 0 /\ d1 - i1 >= 0 /\ -d1 - i1 >= 0 /\ v - i1 >= 0 /\ -v - i1 >= 0 /\ u - i1 >= 0 /\ -u - i1 >= 0 /\ a - i1 - 2 >= 0 /\ i1 >= 0 /\ h1 + i1 >= 0 /\ -h1 + i1 >= 0 /\ g1 + i1 >= 0 /\ -g1 + i1 >= 0 /\ d1 + i1 >= 0 /\ -d1 + i1 >= 0 /\ v + i1 >= 0 /\ -v + i1 >= 0 /\ u + i1 >= 0 /\ -u + i1 >= 0 /\ a + i1 - 2 >= 0 /\ -h1 >= 0 /\ g1 - h1 >= 0 /\ -g1 - h1 >= 0 /\ d1 - h1 >= 0 /\ -d1 - h1 >= 0 /\ v - h1 >= 0 /\ -v - h1 >= 0 /\ u - h1 >= 0 /\ -u - h1 >= 0 /\ a - h1 - 2 >= 0 /\ h1 >= 0 /\ g1 + h1 >= 0 /\ -g1 + h1 >= 0 /\ d1 + h1 >= 0 /\ -d1 + h1 >= 0 /\ v + h1 >= 0 /\ -v + h1 >= 0 /\ u + h1 >= 0 /\ -u + h1 >= 0 /\ a + h1 - 2 >= 0 /\ -g1 >= 0 /\ d1 - g1 >= 0 /\ -d1 - g1 >= 0 /\ v - g1 >= 0 /\ -v - g1 >= 0 /\ u - g1 >= 0 /\ -u - g1 >= 0 /\ a - g1 - 2 >= 0 /\ g1 >= 0 /\ d1 + g1 >= 0 /\ -d1 + g1 >= 0 /\ v + g1 >= 0 /\ -v + g1 >= 0 /\ u + g1 >= 0 /\ -u + g1 >= 0 /\ a + g1 - 2 >= 0 /\ b1 - e1 >= 0 /\ -d1 >= 0 /\ v - d1 >= 0 /\ -v - d1 >= 0 /\ u - d1 >= 0 /\ -u - d1 >= 0 /\ a - d1 - 2 >= 0 /\ d1 >= 0 /\ v + d1 >= 0 /\ -v + d1 >= 0 /\ u + d1 >= 0 /\ -u + d1 >= 0 /\ a + d1 - 2 >= 0 /\ -v >= 0 /\ u - v >= 0 /\ -u - v >= 0 /\ a - v - 2 >= 0 /\ v >= 0 /\ u + v >= 0 /\ -u + v >= 0 /\ a + v - 2 >= 0 /\ -u >= 0 /\ a - u - 2 >= 0 /\ u >= 0 /\ a + u - 2 >= 0 /\ a - 2 >= 0 /\ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(a, b + 1, c, e, f, o, p, q, s, z1, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ b >= 0 /\ q >= b + 1 ] (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(z1, 2, c, e, f, o, 0, z1, s, b2, u, v, s, b1, d1, e1, g1, h1, i1, j1, m1) [ z1 >= 2 /\ s = w ] start location: f9 leaf cost: 6 By chaining the transition f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 12, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 /\ 6 >= 0 /\ e1 - 6 >= 0 /\ 7 >= 0 /\ e1 - 7 >= 0 /\ 8 >= 0 /\ e1 - 8 >= 0 /\ 9 >= 0 /\ e1 - 9 >= 0 /\ 10 >= 0 /\ e1 - 10 >= 0 /\ 11 >= 0 /\ e1 - 11 >= 0 ] with all transitions in problem 21, the following new transition is obtained: f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 13, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 /\ 6 >= 0 /\ e1 - 6 >= 0 /\ 7 >= 0 /\ e1 - 7 >= 0 /\ 8 >= 0 /\ e1 - 8 >= 0 /\ 9 >= 0 /\ e1 - 9 >= 0 /\ 10 >= 0 /\ e1 - 10 >= 0 /\ 11 >= 0 /\ e1 - 11 >= 0 /\ 12 >= 0 /\ e1 - 12 >= 0 ] We thus obtain the following problem: 22: T: (2, 15) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 13, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 /\ 6 >= 0 /\ e1 - 6 >= 0 /\ 7 >= 0 /\ e1 - 7 >= 0 /\ 8 >= 0 /\ e1 - 8 >= 0 /\ 9 >= 0 /\ e1 - 9 >= 0 /\ 10 >= 0 /\ e1 - 10 >= 0 /\ 11 >= 0 /\ e1 - 11 >= 0 /\ 12 >= 0 /\ e1 - 12 >= 0 ] (c + f + e1 + 1, 1) f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, 0, h1, w, b1, d1, e1 - 1, 0, h1, 0, h1, m1) [ -p + 1 >= 0 /\ o - p - 1 >= 0 /\ f - p - 1 >= 0 /\ j1 - p + 1 >= 0 /\ -j1 - p + 1 >= 0 /\ i1 - p + 1 >= 0 /\ -i1 - p + 1 >= 0 /\ h1 - p + 1 >= 0 /\ -h1 - p + 1 >= 0 /\ g1 - p + 1 >= 0 /\ -g1 - p + 1 >= 0 /\ d1 - p + 1 >= 0 /\ -d1 - p + 1 >= 0 /\ v - p + 1 >= 0 /\ -v - p + 1 >= 0 /\ u - p + 1 >= 0 /\ -u - p + 1 >= 0 /\ a - p - 1 >= 0 /\ p - 1 >= 0 /\ o + p - 3 >= 0 /\ f + p - 3 >= 0 /\ j1 + p - 1 >= 0 /\ -j1 + p - 1 >= 0 /\ i1 + p - 1 >= 0 /\ -i1 + p - 1 >= 0 /\ h1 + p - 1 >= 0 /\ -h1 + p - 1 >= 0 /\ g1 + p - 1 >= 0 /\ -g1 + p - 1 >= 0 /\ d1 + p - 1 >= 0 /\ -d1 + p - 1 >= 0 /\ v + p - 1 >= 0 /\ -v + p - 1 >= 0 /\ u + p - 1 >= 0 /\ -u + p - 1 >= 0 /\ a + p - 3 >= 0 /\ f - o >= 0 /\ o - 2 >= 0 /\ f + o - 4 >= 0 /\ -f + o >= 0 /\ j1 + o - 2 >= 0 /\ -j1 + o - 2 >= 0 /\ i1 + o - 2 >= 0 /\ -i1 + o - 2 >= 0 /\ h1 + o - 2 >= 0 /\ -h1 + o - 2 >= 0 /\ g1 + o - 2 >= 0 /\ -g1 + o - 2 >= 0 /\ d1 + o - 2 >= 0 /\ -d1 + o - 2 >= 0 /\ v + o - 2 >= 0 /\ -v + o - 2 >= 0 /\ u + o - 2 >= 0 /\ -u + o - 2 >= 0 /\ a + o - 4 >= 0 /\ -a + o >= 0 /\ f - 2 >= 0 /\ j1 + f - 2 >= 0 /\ -j1 + f - 2 >= 0 /\ i1 + f - 2 >= 0 /\ -i1 + f - 2 >= 0 /\ h1 + f - 2 >= 0 /\ -h1 + f - 2 >= 0 /\ g1 + f - 2 >= 0 /\ -g1 + f - 2 >= 0 /\ d1 + f - 2 >= 0 /\ -d1 + f - 2 >= 0 /\ v + f - 2 >= 0 /\ -v + f - 2 >= 0 /\ u + f - 2 >= 0 /\ -u + f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ b1 - c + 1 >= 0 /\ -e1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -j1 >= 0 /\ i1 - j1 >= 0 /\ -i1 - j1 >= 0 /\ h1 - j1 >= 0 /\ -h1 - j1 >= 0 /\ g1 - j1 >= 0 /\ -g1 - j1 >= 0 /\ d1 - j1 >= 0 /\ -d1 - j1 >= 0 /\ v - j1 >= 0 /\ -v - j1 >= 0 /\ u - j1 >= 0 /\ -u - j1 >= 0 /\ a - j1 - 2 >= 0 /\ j1 >= 0 /\ i1 + j1 >= 0 /\ -i1 + j1 >= 0 /\ h1 + j1 >= 0 /\ -h1 + j1 >= 0 /\ g1 + j1 >= 0 /\ -g1 + j1 >= 0 /\ d1 + j1 >= 0 /\ -d1 + j1 >= 0 /\ v + j1 >= 0 /\ -v + j1 >= 0 /\ u + j1 >= 0 /\ -u + j1 >= 0 /\ a + j1 - 2 >= 0 /\ -i1 >= 0 /\ h1 - i1 >= 0 /\ -h1 - i1 >= 0 /\ g1 - i1 >= 0 /\ -g1 - i1 >= 0 /\ d1 - i1 >= 0 /\ -d1 - i1 >= 0 /\ v - i1 >= 0 /\ -v - i1 >= 0 /\ u - i1 >= 0 /\ -u - i1 >= 0 /\ a - i1 - 2 >= 0 /\ i1 >= 0 /\ h1 + i1 >= 0 /\ -h1 + i1 >= 0 /\ g1 + i1 >= 0 /\ -g1 + i1 >= 0 /\ d1 + i1 >= 0 /\ -d1 + i1 >= 0 /\ v + i1 >= 0 /\ -v + i1 >= 0 /\ u + i1 >= 0 /\ -u + i1 >= 0 /\ a + i1 - 2 >= 0 /\ -h1 >= 0 /\ g1 - h1 >= 0 /\ -g1 - h1 >= 0 /\ d1 - h1 >= 0 /\ -d1 - h1 >= 0 /\ v - h1 >= 0 /\ -v - h1 >= 0 /\ u - h1 >= 0 /\ -u - h1 >= 0 /\ a - h1 - 2 >= 0 /\ h1 >= 0 /\ g1 + h1 >= 0 /\ -g1 + h1 >= 0 /\ d1 + h1 >= 0 /\ -d1 + h1 >= 0 /\ v + h1 >= 0 /\ -v + h1 >= 0 /\ u + h1 >= 0 /\ -u + h1 >= 0 /\ a + h1 - 2 >= 0 /\ -g1 >= 0 /\ d1 - g1 >= 0 /\ -d1 - g1 >= 0 /\ v - g1 >= 0 /\ -v - g1 >= 0 /\ u - g1 >= 0 /\ -u - g1 >= 0 /\ a - g1 - 2 >= 0 /\ g1 >= 0 /\ d1 + g1 >= 0 /\ -d1 + g1 >= 0 /\ v + g1 >= 0 /\ -v + g1 >= 0 /\ u + g1 >= 0 /\ -u + g1 >= 0 /\ a + g1 - 2 >= 0 /\ b1 - e1 >= 0 /\ -d1 >= 0 /\ v - d1 >= 0 /\ -v - d1 >= 0 /\ u - d1 >= 0 /\ -u - d1 >= 0 /\ a - d1 - 2 >= 0 /\ d1 >= 0 /\ v + d1 >= 0 /\ -v + d1 >= 0 /\ u + d1 >= 0 /\ -u + d1 >= 0 /\ a + d1 - 2 >= 0 /\ -v >= 0 /\ u - v >= 0 /\ -u - v >= 0 /\ a - v - 2 >= 0 /\ v >= 0 /\ u + v >= 0 /\ -u + v >= 0 /\ a + v - 2 >= 0 /\ -u >= 0 /\ a - u - 2 >= 0 /\ u >= 0 /\ a + u - 2 >= 0 /\ a - 2 >= 0 /\ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(a, b + 1, c, e, f, o, p, q, s, z1, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ b >= 0 /\ q >= b + 1 ] (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(z1, 2, c, e, f, o, 0, z1, s, b2, u, v, s, b1, d1, e1, g1, h1, i1, j1, m1) [ z1 >= 2 /\ s = w ] start location: f9 leaf cost: 6 By chaining the transition f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 13, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 /\ 6 >= 0 /\ e1 - 6 >= 0 /\ 7 >= 0 /\ e1 - 7 >= 0 /\ 8 >= 0 /\ e1 - 8 >= 0 /\ 9 >= 0 /\ e1 - 9 >= 0 /\ 10 >= 0 /\ e1 - 10 >= 0 /\ 11 >= 0 /\ e1 - 11 >= 0 /\ 12 >= 0 /\ e1 - 12 >= 0 ] with all transitions in problem 22, the following new transition is obtained: f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 14, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 /\ 6 >= 0 /\ e1 - 6 >= 0 /\ 7 >= 0 /\ e1 - 7 >= 0 /\ 8 >= 0 /\ e1 - 8 >= 0 /\ 9 >= 0 /\ e1 - 9 >= 0 /\ 10 >= 0 /\ e1 - 10 >= 0 /\ 11 >= 0 /\ e1 - 11 >= 0 /\ 12 >= 0 /\ e1 - 12 >= 0 /\ 13 >= 0 /\ e1 - 13 >= 0 ] We thus obtain the following problem: 23: T: (2, 16) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, z1, e1 + 1, e, f, f, 1, a2, y1, d2, 0, r, e2, e1, r, e1 - 14, 0, r, 0, r, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ a >= 2 /\ c2 >= a /\ f >= a /\ b >= q /\ b >= 0 /\ c = 0 /\ f - p - 2 >= 0 /\ a - p - 2 >= 0 /\ f + p - 2 >= 0 /\ a + p - 2 >= 0 /\ f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ 0 >= 0 /\ a - 2 >= 0 /\ z1' >= 0 /\ f >= 0 /\ r = 0 /\ p = 0 /\ r >= 0 /\ -r >= 0 /\ 2*f - 4 >= 0 /\ r + f - 2 >= 0 /\ -r + f - 2 >= 0 /\ -2*r >= 0 /\ a - r - 2 >= 0 /\ 2*r >= 0 /\ a + r - 2 >= 0 /\ e1 >= 0 /\ 0 = 0 /\ r = r /\ 1 >= 0 /\ e1 - 1 >= 0 /\ 2 >= 0 /\ e1 - 2 >= 0 /\ 3 >= 0 /\ e1 - 3 >= 0 /\ 4 >= 0 /\ e1 - 4 >= 0 /\ 5 >= 0 /\ e1 - 5 >= 0 /\ 6 >= 0 /\ e1 - 6 >= 0 /\ 7 >= 0 /\ e1 - 7 >= 0 /\ 8 >= 0 /\ e1 - 8 >= 0 /\ 9 >= 0 /\ e1 - 9 >= 0 /\ 10 >= 0 /\ e1 - 10 >= 0 /\ 11 >= 0 /\ e1 - 11 >= 0 /\ 12 >= 0 /\ e1 - 12 >= 0 /\ 13 >= 0 /\ e1 - 13 >= 0 ] (c + f + e1 + 1, 1) f8(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f8(a, b, c, e, f, o, p, q, r, s, 0, h1, w, b1, d1, e1 - 1, 0, h1, 0, h1, m1) [ -p + 1 >= 0 /\ o - p - 1 >= 0 /\ f - p - 1 >= 0 /\ j1 - p + 1 >= 0 /\ -j1 - p + 1 >= 0 /\ i1 - p + 1 >= 0 /\ -i1 - p + 1 >= 0 /\ h1 - p + 1 >= 0 /\ -h1 - p + 1 >= 0 /\ g1 - p + 1 >= 0 /\ -g1 - p + 1 >= 0 /\ d1 - p + 1 >= 0 /\ -d1 - p + 1 >= 0 /\ v - p + 1 >= 0 /\ -v - p + 1 >= 0 /\ u - p + 1 >= 0 /\ -u - p + 1 >= 0 /\ a - p - 1 >= 0 /\ p - 1 >= 0 /\ o + p - 3 >= 0 /\ f + p - 3 >= 0 /\ j1 + p - 1 >= 0 /\ -j1 + p - 1 >= 0 /\ i1 + p - 1 >= 0 /\ -i1 + p - 1 >= 0 /\ h1 + p - 1 >= 0 /\ -h1 + p - 1 >= 0 /\ g1 + p - 1 >= 0 /\ -g1 + p - 1 >= 0 /\ d1 + p - 1 >= 0 /\ -d1 + p - 1 >= 0 /\ v + p - 1 >= 0 /\ -v + p - 1 >= 0 /\ u + p - 1 >= 0 /\ -u + p - 1 >= 0 /\ a + p - 3 >= 0 /\ f - o >= 0 /\ o - 2 >= 0 /\ f + o - 4 >= 0 /\ -f + o >= 0 /\ j1 + o - 2 >= 0 /\ -j1 + o - 2 >= 0 /\ i1 + o - 2 >= 0 /\ -i1 + o - 2 >= 0 /\ h1 + o - 2 >= 0 /\ -h1 + o - 2 >= 0 /\ g1 + o - 2 >= 0 /\ -g1 + o - 2 >= 0 /\ d1 + o - 2 >= 0 /\ -d1 + o - 2 >= 0 /\ v + o - 2 >= 0 /\ -v + o - 2 >= 0 /\ u + o - 2 >= 0 /\ -u + o - 2 >= 0 /\ a + o - 4 >= 0 /\ -a + o >= 0 /\ f - 2 >= 0 /\ j1 + f - 2 >= 0 /\ -j1 + f - 2 >= 0 /\ i1 + f - 2 >= 0 /\ -i1 + f - 2 >= 0 /\ h1 + f - 2 >= 0 /\ -h1 + f - 2 >= 0 /\ g1 + f - 2 >= 0 /\ -g1 + f - 2 >= 0 /\ d1 + f - 2 >= 0 /\ -d1 + f - 2 >= 0 /\ v + f - 2 >= 0 /\ -v + f - 2 >= 0 /\ u + f - 2 >= 0 /\ -u + f - 2 >= 0 /\ a + f - 4 >= 0 /\ -a + f >= 0 /\ b1 - c + 1 >= 0 /\ -e1 + c - 1 >= 0 /\ -b1 + c - 1 >= 0 /\ -j1 >= 0 /\ i1 - j1 >= 0 /\ -i1 - j1 >= 0 /\ h1 - j1 >= 0 /\ -h1 - j1 >= 0 /\ g1 - j1 >= 0 /\ -g1 - j1 >= 0 /\ d1 - j1 >= 0 /\ -d1 - j1 >= 0 /\ v - j1 >= 0 /\ -v - j1 >= 0 /\ u - j1 >= 0 /\ -u - j1 >= 0 /\ a - j1 - 2 >= 0 /\ j1 >= 0 /\ i1 + j1 >= 0 /\ -i1 + j1 >= 0 /\ h1 + j1 >= 0 /\ -h1 + j1 >= 0 /\ g1 + j1 >= 0 /\ -g1 + j1 >= 0 /\ d1 + j1 >= 0 /\ -d1 + j1 >= 0 /\ v + j1 >= 0 /\ -v + j1 >= 0 /\ u + j1 >= 0 /\ -u + j1 >= 0 /\ a + j1 - 2 >= 0 /\ -i1 >= 0 /\ h1 - i1 >= 0 /\ -h1 - i1 >= 0 /\ g1 - i1 >= 0 /\ -g1 - i1 >= 0 /\ d1 - i1 >= 0 /\ -d1 - i1 >= 0 /\ v - i1 >= 0 /\ -v - i1 >= 0 /\ u - i1 >= 0 /\ -u - i1 >= 0 /\ a - i1 - 2 >= 0 /\ i1 >= 0 /\ h1 + i1 >= 0 /\ -h1 + i1 >= 0 /\ g1 + i1 >= 0 /\ -g1 + i1 >= 0 /\ d1 + i1 >= 0 /\ -d1 + i1 >= 0 /\ v + i1 >= 0 /\ -v + i1 >= 0 /\ u + i1 >= 0 /\ -u + i1 >= 0 /\ a + i1 - 2 >= 0 /\ -h1 >= 0 /\ g1 - h1 >= 0 /\ -g1 - h1 >= 0 /\ d1 - h1 >= 0 /\ -d1 - h1 >= 0 /\ v - h1 >= 0 /\ -v - h1 >= 0 /\ u - h1 >= 0 /\ -u - h1 >= 0 /\ a - h1 - 2 >= 0 /\ h1 >= 0 /\ g1 + h1 >= 0 /\ -g1 + h1 >= 0 /\ d1 + h1 >= 0 /\ -d1 + h1 >= 0 /\ v + h1 >= 0 /\ -v + h1 >= 0 /\ u + h1 >= 0 /\ -u + h1 >= 0 /\ a + h1 - 2 >= 0 /\ -g1 >= 0 /\ d1 - g1 >= 0 /\ -d1 - g1 >= 0 /\ v - g1 >= 0 /\ -v - g1 >= 0 /\ u - g1 >= 0 /\ -u - g1 >= 0 /\ a - g1 - 2 >= 0 /\ g1 >= 0 /\ d1 + g1 >= 0 /\ -d1 + g1 >= 0 /\ v + g1 >= 0 /\ -v + g1 >= 0 /\ u + g1 >= 0 /\ -u + g1 >= 0 /\ a + g1 - 2 >= 0 /\ b1 - e1 >= 0 /\ -d1 >= 0 /\ v - d1 >= 0 /\ -v - d1 >= 0 /\ u - d1 >= 0 /\ -u - d1 >= 0 /\ a - d1 - 2 >= 0 /\ d1 >= 0 /\ v + d1 >= 0 /\ -v + d1 >= 0 /\ u + d1 >= 0 /\ -u + d1 >= 0 /\ a + d1 - 2 >= 0 /\ -v >= 0 /\ u - v >= 0 /\ -u - v >= 0 /\ a - v - 2 >= 0 /\ v >= 0 /\ u + v >= 0 /\ -u + v >= 0 /\ a + v - 2 >= 0 /\ -u >= 0 /\ a - u - 2 >= 0 /\ u >= 0 /\ a + u - 2 >= 0 /\ a - 2 >= 0 /\ e1 >= 0 /\ a >= 2 /\ i1 = 0 /\ h1 = v /\ g1 = 0 /\ u = 0 /\ j1 = v ] (?, 1) f1(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(a, b + 1, c, e, f, o, p, q, s, z1, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) [ q - 2 >= 0 /\ p + q - 2 >= 0 /\ -p + q - 2 >= 0 /\ b + q - 4 >= 0 /\ -b + q >= 0 /\ -p >= 0 /\ b - p - 2 >= 0 /\ p >= 0 /\ b + p - 2 >= 0 /\ b - 2 >= 0 /\ b >= 0 /\ q >= b + 1 ] (1, 1) f9(a, b, c, e, f, o, p, q, r, s, u, v, w, b1, d1, e1, g1, h1, i1, j1, m1) -> f1(z1, 2, c, e, f, o, 0, z1, s, b2, u, v, s, b1, d1, e1, g1, h1, i1, j1, m1) [ z1 >= 2 /\ s = w ] start location: f9 leaf cost: 6 Complexity upper bound ? Time: 10.619 sec (SMT: 7.915 sec)