YES(?, 12*a + 12*c + 6*e + 2*a*e + 2*c*e + 26) Initial complexity problem: 1: T: (?, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> stop(a, b, c, d, e, f, g, h, i, j, k, l) [ 0 >= a + 1 /\ b = c /\ d = e /\ f = g /\ h = i /\ j = k /\ l = a ] (?, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> stop(a, b, c, d, e, f, g, h, i, j, k, l) [ 0 >= e + 1 /\ b = c /\ d = e /\ f = g /\ h = i /\ j = k /\ l = a ] (?, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> stop(a, b, c, d, e, f, g, h, i, j, k, l) [ 0 >= c + 1 /\ b = c /\ d = e /\ f = g /\ h = i /\ j = k /\ l = a ] (?, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> stop(a, b, c, d, e, f, g, h, i, 0, k, l) [ a >= 0 /\ e >= 0 /\ b = 0 /\ c = 0 /\ d = e /\ f = g /\ h = i /\ j = k /\ l = a ] (?, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, 1, k, l) [ a >= 0 /\ c >= 1 /\ d = 0 /\ b = c /\ e = 0 /\ f = g /\ h = i /\ j = k /\ l = a ] (?, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, 0, g, 1, i, 0, k, l) [ e >= 1 /\ c >= 1 /\ l = 0 /\ b = c /\ d = e /\ f = g /\ h = i /\ j = k /\ a = 0 ] (?, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, 1, g, 1, i, 0, k, l) [ a >= 1 /\ e >= 1 /\ c >= 1 /\ b = c /\ d = e /\ f = g /\ h = i /\ j = k /\ l = a ] (?, 1) lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> stop(a, b, c, d, e, f, g, h, i, j, k, l) [ j >= c /\ e >= 0 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = e /\ l = a /\ d = e /\ b = c ] (?, 1) lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, j + 1, k, l) [ c >= j + 1 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = 0 /\ d = 0 /\ l = a /\ e = 0 /\ b = c ] (?, 1) lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, 1, i, j, k, l) [ e >= 1 /\ c >= j + 1 /\ j >= a /\ e >= 0 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = e /\ l = a /\ d = e /\ b = c ] (?, 1) lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, j + 1, g, 1, i, j, k, l) [ a >= j + 1 /\ e >= 1 /\ c >= j + 1 /\ e >= 0 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = e /\ l = a /\ d = e /\ b = c ] (?, 1) lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, h, i, j + 1, k, l) [ a + c >= f + 1 /\ a >= 0 /\ f >= a /\ e >= 1 /\ h = e /\ j = f /\ l = a /\ d = e /\ b = c ] (?, 1) lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, h + 1, i, j, k, l) [ e >= h + 1 /\ f >= a /\ a + c >= f + 1 /\ a >= 0 /\ e >= h /\ h >= 1 /\ j = f /\ l = a /\ d = e /\ b = c ] (?, 1) lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, j + 1, g, h + 1, i, j, k, l) [ a >= f + 1 /\ e >= h + 1 /\ a + c >= f + 1 /\ a >= 0 /\ e >= h /\ f >= a /\ h >= 1 /\ j = f /\ l = a /\ d = e /\ b = c ] (?, 1) lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, f, g, h, i, f, k, l) [ a >= j + 1 /\ e >= 1 /\ j >= 0 /\ c >= j + 1 /\ f = a /\ h = 1 /\ l = a /\ d = e /\ b = c ] (?, 1) lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, f + 1, g, h, i, j, k, l) [ a >= f + 1 /\ f >= j + 1 /\ e >= 1 /\ j >= 0 /\ a >= f /\ c >= j + 1 /\ h = 1 /\ l = a /\ d = e /\ b = c ] (1, 1) start0(a, b, c, d, e, f, g, h, i, j, k, l) -> start(a, c, c, e, e, g, g, i, i, k, k, a) start location: start0 leaf cost: 0 Testing for unsatisfiable constraints removes the following transition from problem 1: lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, j + 1, g, h + 1, i, j, k, l) [ a >= f + 1 /\ e >= h + 1 /\ a + c >= f + 1 /\ a >= 0 /\ e >= h /\ f >= a /\ h >= 1 /\ j = f /\ l = a /\ d = e /\ b = c ] We thus obtain the following problem: 2: T: (?, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> stop(a, b, c, d, e, f, g, h, i, j, k, l) [ 0 >= a + 1 /\ b = c /\ d = e /\ f = g /\ h = i /\ j = k /\ l = a ] (?, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> stop(a, b, c, d, e, f, g, h, i, j, k, l) [ 0 >= e + 1 /\ b = c /\ d = e /\ f = g /\ h = i /\ j = k /\ l = a ] (?, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> stop(a, b, c, d, e, f, g, h, i, j, k, l) [ 0 >= c + 1 /\ b = c /\ d = e /\ f = g /\ h = i /\ j = k /\ l = a ] (?, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> stop(a, b, c, d, e, f, g, h, i, 0, k, l) [ a >= 0 /\ e >= 0 /\ b = 0 /\ c = 0 /\ d = e /\ f = g /\ h = i /\ j = k /\ l = a ] (?, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, 1, k, l) [ a >= 0 /\ c >= 1 /\ d = 0 /\ b = c /\ e = 0 /\ f = g /\ h = i /\ j = k /\ l = a ] (?, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, 0, g, 1, i, 0, k, l) [ e >= 1 /\ c >= 1 /\ l = 0 /\ b = c /\ d = e /\ f = g /\ h = i /\ j = k /\ a = 0 ] (?, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, 1, g, 1, i, 0, k, l) [ a >= 1 /\ e >= 1 /\ c >= 1 /\ b = c /\ d = e /\ f = g /\ h = i /\ j = k /\ l = a ] (?, 1) lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> stop(a, b, c, d, e, f, g, h, i, j, k, l) [ j >= c /\ e >= 0 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = e /\ l = a /\ d = e /\ b = c ] (?, 1) lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, j + 1, k, l) [ c >= j + 1 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = 0 /\ d = 0 /\ l = a /\ e = 0 /\ b = c ] (?, 1) lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, 1, i, j, k, l) [ e >= 1 /\ c >= j + 1 /\ j >= a /\ e >= 0 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = e /\ l = a /\ d = e /\ b = c ] (?, 1) lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, j + 1, g, 1, i, j, k, l) [ a >= j + 1 /\ e >= 1 /\ c >= j + 1 /\ e >= 0 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = e /\ l = a /\ d = e /\ b = c ] (?, 1) lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, h, i, j + 1, k, l) [ a + c >= f + 1 /\ a >= 0 /\ f >= a /\ e >= 1 /\ h = e /\ j = f /\ l = a /\ d = e /\ b = c ] (?, 1) lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, h + 1, i, j, k, l) [ e >= h + 1 /\ f >= a /\ a + c >= f + 1 /\ a >= 0 /\ e >= h /\ h >= 1 /\ j = f /\ l = a /\ d = e /\ b = c ] (?, 1) lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, f, g, h, i, f, k, l) [ a >= j + 1 /\ e >= 1 /\ j >= 0 /\ c >= j + 1 /\ f = a /\ h = 1 /\ l = a /\ d = e /\ b = c ] (?, 1) lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, f + 1, g, h, i, j, k, l) [ a >= f + 1 /\ f >= j + 1 /\ e >= 1 /\ j >= 0 /\ a >= f /\ c >= j + 1 /\ h = 1 /\ l = a /\ d = e /\ b = c ] (1, 1) start0(a, b, c, d, e, f, g, h, i, j, k, l) -> start(a, c, c, e, e, g, g, i, i, k, k, a) start location: start0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (?, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, 1, k, l) [ a >= 0 /\ c >= 1 /\ d = 0 /\ b = c /\ e = 0 /\ f = g /\ h = i /\ j = k /\ l = a ] (?, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, 0, g, 1, i, 0, k, l) [ e >= 1 /\ c >= 1 /\ l = 0 /\ b = c /\ d = e /\ f = g /\ h = i /\ j = k /\ a = 0 ] (?, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, 1, g, 1, i, 0, k, l) [ a >= 1 /\ e >= 1 /\ c >= 1 /\ b = c /\ d = e /\ f = g /\ h = i /\ j = k /\ l = a ] (?, 1) lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, j + 1, k, l) [ c >= j + 1 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = 0 /\ d = 0 /\ l = a /\ e = 0 /\ b = c ] (?, 1) lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, 1, i, j, k, l) [ e >= 1 /\ c >= j + 1 /\ j >= a /\ e >= 0 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = e /\ l = a /\ d = e /\ b = c ] (?, 1) lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, j + 1, g, 1, i, j, k, l) [ a >= j + 1 /\ e >= 1 /\ c >= j + 1 /\ e >= 0 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = e /\ l = a /\ d = e /\ b = c ] (?, 1) lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, h, i, j + 1, k, l) [ a + c >= f + 1 /\ a >= 0 /\ f >= a /\ e >= 1 /\ h = e /\ j = f /\ l = a /\ d = e /\ b = c ] (?, 1) lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, h + 1, i, j, k, l) [ e >= h + 1 /\ f >= a /\ a + c >= f + 1 /\ a >= 0 /\ e >= h /\ h >= 1 /\ j = f /\ l = a /\ d = e /\ b = c ] (?, 1) lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, f, g, h, i, f, k, l) [ a >= j + 1 /\ e >= 1 /\ j >= 0 /\ c >= j + 1 /\ f = a /\ h = 1 /\ l = a /\ d = e /\ b = c ] (?, 1) lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, f + 1, g, h, i, j, k, l) [ a >= f + 1 /\ f >= j + 1 /\ e >= 1 /\ j >= 0 /\ a >= f /\ c >= j + 1 /\ h = 1 /\ l = a /\ d = e /\ b = c ] (1, 1) start0(a, b, c, d, e, f, g, h, i, j, k, l) -> start(a, c, c, e, e, g, g, i, i, k, k, a) start location: start0 leaf cost: 5 Testing for reachability in the complexity graph removes the following transition from problem 3: lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, j + 1, g, 1, i, j, k, l) [ a >= j + 1 /\ e >= 1 /\ c >= j + 1 /\ e >= 0 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = e /\ l = a /\ d = e /\ b = c ] We thus obtain the following problem: 4: T: (?, 1) lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, 1, i, j, k, l) [ e >= 1 /\ c >= j + 1 /\ j >= a /\ e >= 0 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = e /\ l = a /\ d = e /\ b = c ] (?, 1) lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, f + 1, g, h, i, j, k, l) [ a >= f + 1 /\ f >= j + 1 /\ e >= 1 /\ j >= 0 /\ a >= f /\ c >= j + 1 /\ h = 1 /\ l = a /\ d = e /\ b = c ] (?, 1) lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, f, g, h, i, f, k, l) [ a >= j + 1 /\ e >= 1 /\ j >= 0 /\ c >= j + 1 /\ f = a /\ h = 1 /\ l = a /\ d = e /\ b = c ] (?, 1) lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, h + 1, i, j, k, l) [ e >= h + 1 /\ f >= a /\ a + c >= f + 1 /\ a >= 0 /\ e >= h /\ h >= 1 /\ j = f /\ l = a /\ d = e /\ b = c ] (?, 1) lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, h, i, j + 1, k, l) [ a + c >= f + 1 /\ a >= 0 /\ f >= a /\ e >= 1 /\ h = e /\ j = f /\ l = a /\ d = e /\ b = c ] (?, 1) lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, j + 1, k, l) [ c >= j + 1 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = 0 /\ d = 0 /\ l = a /\ e = 0 /\ b = c ] (?, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, 1, g, 1, i, 0, k, l) [ a >= 1 /\ e >= 1 /\ c >= 1 /\ b = c /\ d = e /\ f = g /\ h = i /\ j = k /\ l = a ] (?, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, 0, g, 1, i, 0, k, l) [ e >= 1 /\ c >= 1 /\ l = 0 /\ b = c /\ d = e /\ f = g /\ h = i /\ j = k /\ a = 0 ] (?, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, 1, k, l) [ a >= 0 /\ c >= 1 /\ d = 0 /\ b = c /\ e = 0 /\ f = g /\ h = i /\ j = k /\ l = a ] (1, 1) start0(a, b, c, d, e, f, g, h, i, j, k, l) -> start(a, c, c, e, e, g, g, i, i, k, k, a) start location: start0 leaf cost: 5 Repeatedly propagating knowledge in problem 4 produces the following problem: 5: T: (?, 1) lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, 1, i, j, k, l) [ e >= 1 /\ c >= j + 1 /\ j >= a /\ e >= 0 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = e /\ l = a /\ d = e /\ b = c ] (?, 1) lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, f + 1, g, h, i, j, k, l) [ a >= f + 1 /\ f >= j + 1 /\ e >= 1 /\ j >= 0 /\ a >= f /\ c >= j + 1 /\ h = 1 /\ l = a /\ d = e /\ b = c ] (?, 1) lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, f, g, h, i, f, k, l) [ a >= j + 1 /\ e >= 1 /\ j >= 0 /\ c >= j + 1 /\ f = a /\ h = 1 /\ l = a /\ d = e /\ b = c ] (?, 1) lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, h + 1, i, j, k, l) [ e >= h + 1 /\ f >= a /\ a + c >= f + 1 /\ a >= 0 /\ e >= h /\ h >= 1 /\ j = f /\ l = a /\ d = e /\ b = c ] (?, 1) lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, h, i, j + 1, k, l) [ a + c >= f + 1 /\ a >= 0 /\ f >= a /\ e >= 1 /\ h = e /\ j = f /\ l = a /\ d = e /\ b = c ] (?, 1) lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, j + 1, k, l) [ c >= j + 1 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = 0 /\ d = 0 /\ l = a /\ e = 0 /\ b = c ] (1, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, 1, g, 1, i, 0, k, l) [ a >= 1 /\ e >= 1 /\ c >= 1 /\ b = c /\ d = e /\ f = g /\ h = i /\ j = k /\ l = a ] (1, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, 0, g, 1, i, 0, k, l) [ e >= 1 /\ c >= 1 /\ l = 0 /\ b = c /\ d = e /\ f = g /\ h = i /\ j = k /\ a = 0 ] (1, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, 1, k, l) [ a >= 0 /\ c >= 1 /\ d = 0 /\ b = c /\ e = 0 /\ f = g /\ h = i /\ j = k /\ l = a ] (1, 1) start0(a, b, c, d, e, f, g, h, i, j, k, l) -> start(a, c, c, e, e, g, g, i, i, k, k, a) start location: start0 leaf cost: 5 A polynomial rank function with Pol(lbl131) = 4 Pol(lbl121) = 4 Pol(lbl111) = 5 Pol(start) = 5 Pol(start0) = 5 orients all transitions weakly and the transition lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, f, g, h, i, f, k, l) [ a >= j + 1 /\ e >= 1 /\ j >= 0 /\ c >= j + 1 /\ f = a /\ h = 1 /\ l = a /\ d = e /\ b = c ] strictly and produces the following problem: 6: T: (?, 1) lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, 1, i, j, k, l) [ e >= 1 /\ c >= j + 1 /\ j >= a /\ e >= 0 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = e /\ l = a /\ d = e /\ b = c ] (?, 1) lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, f + 1, g, h, i, j, k, l) [ a >= f + 1 /\ f >= j + 1 /\ e >= 1 /\ j >= 0 /\ a >= f /\ c >= j + 1 /\ h = 1 /\ l = a /\ d = e /\ b = c ] (5, 1) lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, f, g, h, i, f, k, l) [ a >= j + 1 /\ e >= 1 /\ j >= 0 /\ c >= j + 1 /\ f = a /\ h = 1 /\ l = a /\ d = e /\ b = c ] (?, 1) lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, h + 1, i, j, k, l) [ e >= h + 1 /\ f >= a /\ a + c >= f + 1 /\ a >= 0 /\ e >= h /\ h >= 1 /\ j = f /\ l = a /\ d = e /\ b = c ] (?, 1) lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, h, i, j + 1, k, l) [ a + c >= f + 1 /\ a >= 0 /\ f >= a /\ e >= 1 /\ h = e /\ j = f /\ l = a /\ d = e /\ b = c ] (?, 1) lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, j + 1, k, l) [ c >= j + 1 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = 0 /\ d = 0 /\ l = a /\ e = 0 /\ b = c ] (1, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, 1, g, 1, i, 0, k, l) [ a >= 1 /\ e >= 1 /\ c >= 1 /\ b = c /\ d = e /\ f = g /\ h = i /\ j = k /\ l = a ] (1, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, 0, g, 1, i, 0, k, l) [ e >= 1 /\ c >= 1 /\ l = 0 /\ b = c /\ d = e /\ f = g /\ h = i /\ j = k /\ a = 0 ] (1, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, 1, k, l) [ a >= 0 /\ c >= 1 /\ d = 0 /\ b = c /\ e = 0 /\ f = g /\ h = i /\ j = k /\ l = a ] (1, 1) start0(a, b, c, d, e, f, g, h, i, j, k, l) -> start(a, c, c, e, e, g, g, i, i, k, k, a) start location: start0 leaf cost: 5 A polynomial rank function with Pol(lbl131) = 2*V_1 + 2*V_3 - 2*V_10 + 1 Pol(lbl121) = 2*V_1 + 2*V_3 - 2*V_10 Pol(lbl111) = 2*V_1 + 2*V_3 - 2*V_6 + 2 Pol(start) = 2*V_1 + 2*V_3 Pol(start0) = 2*V_1 + 2*V_3 orients all transitions weakly and the transitions lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, j + 1, k, l) [ c >= j + 1 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = 0 /\ d = 0 /\ l = a /\ e = 0 /\ b = c ] lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, 1, i, j, k, l) [ e >= 1 /\ c >= j + 1 /\ j >= a /\ e >= 0 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = e /\ l = a /\ d = e /\ b = c ] lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, h, i, j + 1, k, l) [ a + c >= f + 1 /\ a >= 0 /\ f >= a /\ e >= 1 /\ h = e /\ j = f /\ l = a /\ d = e /\ b = c ] lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, f + 1, g, h, i, j, k, l) [ a >= f + 1 /\ f >= j + 1 /\ e >= 1 /\ j >= 0 /\ a >= f /\ c >= j + 1 /\ h = 1 /\ l = a /\ d = e /\ b = c ] strictly and produces the following problem: 7: T: (2*a + 2*c, 1) lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, 1, i, j, k, l) [ e >= 1 /\ c >= j + 1 /\ j >= a /\ e >= 0 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = e /\ l = a /\ d = e /\ b = c ] (2*a + 2*c, 1) lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, f + 1, g, h, i, j, k, l) [ a >= f + 1 /\ f >= j + 1 /\ e >= 1 /\ j >= 0 /\ a >= f /\ c >= j + 1 /\ h = 1 /\ l = a /\ d = e /\ b = c ] (5, 1) lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, f, g, h, i, f, k, l) [ a >= j + 1 /\ e >= 1 /\ j >= 0 /\ c >= j + 1 /\ f = a /\ h = 1 /\ l = a /\ d = e /\ b = c ] (?, 1) lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, h + 1, i, j, k, l) [ e >= h + 1 /\ f >= a /\ a + c >= f + 1 /\ a >= 0 /\ e >= h /\ h >= 1 /\ j = f /\ l = a /\ d = e /\ b = c ] (2*a + 2*c, 1) lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, h, i, j + 1, k, l) [ a + c >= f + 1 /\ a >= 0 /\ f >= a /\ e >= 1 /\ h = e /\ j = f /\ l = a /\ d = e /\ b = c ] (2*a + 2*c, 1) lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, j + 1, k, l) [ c >= j + 1 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = 0 /\ d = 0 /\ l = a /\ e = 0 /\ b = c ] (1, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, 1, g, 1, i, 0, k, l) [ a >= 1 /\ e >= 1 /\ c >= 1 /\ b = c /\ d = e /\ f = g /\ h = i /\ j = k /\ l = a ] (1, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, 0, g, 1, i, 0, k, l) [ e >= 1 /\ c >= 1 /\ l = 0 /\ b = c /\ d = e /\ f = g /\ h = i /\ j = k /\ a = 0 ] (1, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, 1, k, l) [ a >= 0 /\ c >= 1 /\ d = 0 /\ b = c /\ e = 0 /\ f = g /\ h = i /\ j = k /\ l = a ] (1, 1) start0(a, b, c, d, e, f, g, h, i, j, k, l) -> start(a, c, c, e, e, g, g, i, i, k, k, a) start location: start0 leaf cost: 5 A polynomial rank function with Pol(lbl121) = V_5 - V_8 + 1 and size complexities S("start0(a, b, c, d, e, f, g, h, i, j, k, l) -> start(a, c, c, e, e, g, g, i, i, k, k, a)", 0-0) = a S("start0(a, b, c, d, e, f, g, h, i, j, k, l) -> start(a, c, c, e, e, g, g, i, i, k, k, a)", 0-1) = c S("start0(a, b, c, d, e, f, g, h, i, j, k, l) -> start(a, c, c, e, e, g, g, i, i, k, k, a)", 0-2) = c S("start0(a, b, c, d, e, f, g, h, i, j, k, l) -> start(a, c, c, e, e, g, g, i, i, k, k, a)", 0-3) = e S("start0(a, b, c, d, e, f, g, h, i, j, k, l) -> start(a, c, c, e, e, g, g, i, i, k, k, a)", 0-4) = e S("start0(a, b, c, d, e, f, g, h, i, j, k, l) -> start(a, c, c, e, e, g, g, i, i, k, k, a)", 0-5) = g S("start0(a, b, c, d, e, f, g, h, i, j, k, l) -> start(a, c, c, e, e, g, g, i, i, k, k, a)", 0-6) = g S("start0(a, b, c, d, e, f, g, h, i, j, k, l) -> start(a, c, c, e, e, g, g, i, i, k, k, a)", 0-7) = i S("start0(a, b, c, d, e, f, g, h, i, j, k, l) -> start(a, c, c, e, e, g, g, i, i, k, k, a)", 0-8) = i S("start0(a, b, c, d, e, f, g, h, i, j, k, l) -> start(a, c, c, e, e, g, g, i, i, k, k, a)", 0-9) = k S("start0(a, b, c, d, e, f, g, h, i, j, k, l) -> start(a, c, c, e, e, g, g, i, i, k, k, a)", 0-10) = k S("start0(a, b, c, d, e, f, g, h, i, j, k, l) -> start(a, c, c, e, e, g, g, i, i, k, k, a)", 0-11) = a S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, 1, k, l) [ a >= 0 /\\ c >= 1 /\\ d = 0 /\\ b = c /\\ e = 0 /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-0) = a S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, 1, k, l) [ a >= 0 /\\ c >= 1 /\\ d = 0 /\\ b = c /\\ e = 0 /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-1) = c S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, 1, k, l) [ a >= 0 /\\ c >= 1 /\\ d = 0 /\\ b = c /\\ e = 0 /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-2) = c S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, 1, k, l) [ a >= 0 /\\ c >= 1 /\\ d = 0 /\\ b = c /\\ e = 0 /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-3) = 0 S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, 1, k, l) [ a >= 0 /\\ c >= 1 /\\ d = 0 /\\ b = c /\\ e = 0 /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-4) = 0 S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, 1, k, l) [ a >= 0 /\\ c >= 1 /\\ d = 0 /\\ b = c /\\ e = 0 /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-5) = g S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, 1, k, l) [ a >= 0 /\\ c >= 1 /\\ d = 0 /\\ b = c /\\ e = 0 /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-6) = g S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, 1, k, l) [ a >= 0 /\\ c >= 1 /\\ d = 0 /\\ b = c /\\ e = 0 /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-7) = 0 S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, 1, k, l) [ a >= 0 /\\ c >= 1 /\\ d = 0 /\\ b = c /\\ e = 0 /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-8) = i S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, 1, k, l) [ a >= 0 /\\ c >= 1 /\\ d = 0 /\\ b = c /\\ e = 0 /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-9) = 1 S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, 1, k, l) [ a >= 0 /\\ c >= 1 /\\ d = 0 /\\ b = c /\\ e = 0 /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-10) = k S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, 1, k, l) [ a >= 0 /\\ c >= 1 /\\ d = 0 /\\ b = c /\\ e = 0 /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-11) = a S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, 0, g, 1, i, 0, k, l) [ e >= 1 /\\ c >= 1 /\\ l = 0 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ a = 0 ]", 0-0) = 0 S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, 0, g, 1, i, 0, k, l) [ e >= 1 /\\ c >= 1 /\\ l = 0 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ a = 0 ]", 0-1) = c S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, 0, g, 1, i, 0, k, l) [ e >= 1 /\\ c >= 1 /\\ l = 0 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ a = 0 ]", 0-2) = c S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, 0, g, 1, i, 0, k, l) [ e >= 1 /\\ c >= 1 /\\ l = 0 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ a = 0 ]", 0-3) = e S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, 0, g, 1, i, 0, k, l) [ e >= 1 /\\ c >= 1 /\\ l = 0 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ a = 0 ]", 0-4) = e S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, 0, g, 1, i, 0, k, l) [ e >= 1 /\\ c >= 1 /\\ l = 0 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ a = 0 ]", 0-5) = 0 S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, 0, g, 1, i, 0, k, l) [ e >= 1 /\\ c >= 1 /\\ l = 0 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ a = 0 ]", 0-6) = g S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, 0, g, 1, i, 0, k, l) [ e >= 1 /\\ c >= 1 /\\ l = 0 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ a = 0 ]", 0-7) = 1 S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, 0, g, 1, i, 0, k, l) [ e >= 1 /\\ c >= 1 /\\ l = 0 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ a = 0 ]", 0-8) = i S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, 0, g, 1, i, 0, k, l) [ e >= 1 /\\ c >= 1 /\\ l = 0 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ a = 0 ]", 0-9) = 0 S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, 0, g, 1, i, 0, k, l) [ e >= 1 /\\ c >= 1 /\\ l = 0 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ a = 0 ]", 0-10) = k S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, 0, g, 1, i, 0, k, l) [ e >= 1 /\\ c >= 1 /\\ l = 0 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ a = 0 ]", 0-11) = 0 S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, 1, g, 1, i, 0, k, l) [ a >= 1 /\\ e >= 1 /\\ c >= 1 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-0) = a S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, 1, g, 1, i, 0, k, l) [ a >= 1 /\\ e >= 1 /\\ c >= 1 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-1) = c S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, 1, g, 1, i, 0, k, l) [ a >= 1 /\\ e >= 1 /\\ c >= 1 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-2) = c S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, 1, g, 1, i, 0, k, l) [ a >= 1 /\\ e >= 1 /\\ c >= 1 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-3) = e S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, 1, g, 1, i, 0, k, l) [ a >= 1 /\\ e >= 1 /\\ c >= 1 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-4) = e S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, 1, g, 1, i, 0, k, l) [ a >= 1 /\\ e >= 1 /\\ c >= 1 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-5) = 1 S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, 1, g, 1, i, 0, k, l) [ a >= 1 /\\ e >= 1 /\\ c >= 1 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-6) = g S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, 1, g, 1, i, 0, k, l) [ a >= 1 /\\ e >= 1 /\\ c >= 1 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-7) = 1 S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, 1, g, 1, i, 0, k, l) [ a >= 1 /\\ e >= 1 /\\ c >= 1 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-8) = i S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, 1, g, 1, i, 0, k, l) [ a >= 1 /\\ e >= 1 /\\ c >= 1 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-9) = 0 S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, 1, g, 1, i, 0, k, l) [ a >= 1 /\\ e >= 1 /\\ c >= 1 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-10) = k S("start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, 1, g, 1, i, 0, k, l) [ a >= 1 /\\ e >= 1 /\\ c >= 1 /\\ b = c /\\ d = e /\\ f = g /\\ h = i /\\ j = k /\\ l = a ]", 0-11) = a S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, j + 1, k, l) [ c >= j + 1 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = 0 /\\ d = 0 /\\ l = a /\\ e = 0 /\\ b = c ]", 0-0) = a S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, j + 1, k, l) [ c >= j + 1 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = 0 /\\ d = 0 /\\ l = a /\\ e = 0 /\\ b = c ]", 0-1) = c S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, j + 1, k, l) [ c >= j + 1 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = 0 /\\ d = 0 /\\ l = a /\\ e = 0 /\\ b = c ]", 0-2) = c S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, j + 1, k, l) [ c >= j + 1 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = 0 /\\ d = 0 /\\ l = a /\\ e = 0 /\\ b = c ]", 0-3) = 0 S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, j + 1, k, l) [ c >= j + 1 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = 0 /\\ d = 0 /\\ l = a /\\ e = 0 /\\ b = c ]", 0-4) = 0 S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, j + 1, k, l) [ c >= j + 1 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = 0 /\\ d = 0 /\\ l = a /\\ e = 0 /\\ b = c ]", 0-5) = g S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, j + 1, k, l) [ c >= j + 1 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = 0 /\\ d = 0 /\\ l = a /\\ e = 0 /\\ b = c ]", 0-6) = g S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, j + 1, k, l) [ c >= j + 1 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = 0 /\\ d = 0 /\\ l = a /\\ e = 0 /\\ b = c ]", 0-7) = 0 S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, j + 1, k, l) [ c >= j + 1 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = 0 /\\ d = 0 /\\ l = a /\\ e = 0 /\\ b = c ]", 0-8) = i S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, j + 1, k, l) [ c >= j + 1 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = 0 /\\ d = 0 /\\ l = a /\\ e = 0 /\\ b = c ]", 0-9) = c S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, j + 1, k, l) [ c >= j + 1 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = 0 /\\ d = 0 /\\ l = a /\\ e = 0 /\\ b = c ]", 0-10) = k S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, j + 1, k, l) [ c >= j + 1 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = 0 /\\ d = 0 /\\ l = a /\\ e = 0 /\\ b = c ]", 0-11) = a S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, h, i, j + 1, k, l) [ a + c >= f + 1 /\\ a >= 0 /\\ f >= a /\\ e >= 1 /\\ h = e /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-0) = a S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, h, i, j + 1, k, l) [ a + c >= f + 1 /\\ a >= 0 /\\ f >= a /\\ e >= 1 /\\ h = e /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-1) = c S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, h, i, j + 1, k, l) [ a + c >= f + 1 /\\ a >= 0 /\\ f >= a /\\ e >= 1 /\\ h = e /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-2) = c S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, h, i, j + 1, k, l) [ a + c >= f + 1 /\\ a >= 0 /\\ f >= a /\\ e >= 1 /\\ h = e /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-3) = e S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, h, i, j + 1, k, l) [ a + c >= f + 1 /\\ a >= 0 /\\ f >= a /\\ e >= 1 /\\ h = e /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-4) = e S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, h, i, j + 1, k, l) [ a + c >= f + 1 /\\ a >= 0 /\\ f >= a /\\ e >= 1 /\\ h = e /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-5) = 3*a + 3*c + 81 S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, h, i, j + 1, k, l) [ a + c >= f + 1 /\\ a >= 0 /\\ f >= a /\\ e >= 1 /\\ h = e /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-6) = g S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, h, i, j + 1, k, l) [ a + c >= f + 1 /\\ a >= 0 /\\ f >= a /\\ e >= 1 /\\ h = e /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-7) = e + 3 S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, h, i, j + 1, k, l) [ a + c >= f + 1 /\\ a >= 0 /\\ f >= a /\\ e >= 1 /\\ h = e /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-8) = i S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, h, i, j + 1, k, l) [ a + c >= f + 1 /\\ a >= 0 /\\ f >= a /\\ e >= 1 /\\ h = e /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-9) = 3*a + 3*c + 9 S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, h, i, j + 1, k, l) [ a + c >= f + 1 /\\ a >= 0 /\\ f >= a /\\ e >= 1 /\\ h = e /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-10) = k S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, h, i, j + 1, k, l) [ a + c >= f + 1 /\\ a >= 0 /\\ f >= a /\\ e >= 1 /\\ h = e /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-11) = a S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, h + 1, i, j, k, l) [ e >= h + 1 /\\ f >= a /\\ a + c >= f + 1 /\\ a >= 0 /\\ e >= h /\\ h >= 1 /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-0) = a S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, h + 1, i, j, k, l) [ e >= h + 1 /\\ f >= a /\\ a + c >= f + 1 /\\ a >= 0 /\\ e >= h /\\ h >= 1 /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-1) = c S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, h + 1, i, j, k, l) [ e >= h + 1 /\\ f >= a /\\ a + c >= f + 1 /\\ a >= 0 /\\ e >= h /\\ h >= 1 /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-2) = c S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, h + 1, i, j, k, l) [ e >= h + 1 /\\ f >= a /\\ a + c >= f + 1 /\\ a >= 0 /\\ e >= h /\\ h >= 1 /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-3) = e S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, h + 1, i, j, k, l) [ e >= h + 1 /\\ f >= a /\\ a + c >= f + 1 /\\ a >= 0 /\\ e >= h /\\ h >= 1 /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-4) = e S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, h + 1, i, j, k, l) [ e >= h + 1 /\\ f >= a /\\ a + c >= f + 1 /\\ a >= 0 /\\ e >= h /\\ h >= 1 /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-5) = 3*a + 3*c + 27 S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, h + 1, i, j, k, l) [ e >= h + 1 /\\ f >= a /\\ a + c >= f + 1 /\\ a >= 0 /\\ e >= h /\\ h >= 1 /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-6) = g S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, h + 1, i, j, k, l) [ e >= h + 1 /\\ f >= a /\\ a + c >= f + 1 /\\ a >= 0 /\\ e >= h /\\ h >= 1 /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-7) = e S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, h + 1, i, j, k, l) [ e >= h + 1 /\\ f >= a /\\ a + c >= f + 1 /\\ a >= 0 /\\ e >= h /\\ h >= 1 /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-8) = i S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, h + 1, i, j, k, l) [ e >= h + 1 /\\ f >= a /\\ a + c >= f + 1 /\\ a >= 0 /\\ e >= h /\\ h >= 1 /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-9) = 3*a + 3*c + 9 S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, h + 1, i, j, k, l) [ e >= h + 1 /\\ f >= a /\\ a + c >= f + 1 /\\ a >= 0 /\\ e >= h /\\ h >= 1 /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-10) = k S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, h + 1, i, j, k, l) [ e >= h + 1 /\\ f >= a /\\ a + c >= f + 1 /\\ a >= 0 /\\ e >= h /\\ h >= 1 /\\ j = f /\\ l = a /\\ d = e /\\ b = c ]", 0-11) = a S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, f, g, h, i, f, k, l) [ a >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ c >= j + 1 /\\ f = a /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-0) = a S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, f, g, h, i, f, k, l) [ a >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ c >= j + 1 /\\ f = a /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-1) = c S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, f, g, h, i, f, k, l) [ a >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ c >= j + 1 /\\ f = a /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-2) = c S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, f, g, h, i, f, k, l) [ a >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ c >= j + 1 /\\ f = a /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-3) = e S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, f, g, h, i, f, k, l) [ a >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ c >= j + 1 /\\ f = a /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-4) = e S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, f, g, h, i, f, k, l) [ a >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ c >= j + 1 /\\ f = a /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-5) = a + 1 S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, f, g, h, i, f, k, l) [ a >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ c >= j + 1 /\\ f = a /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-6) = g S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, f, g, h, i, f, k, l) [ a >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ c >= j + 1 /\\ f = a /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-7) = 1 S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, f, g, h, i, f, k, l) [ a >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ c >= j + 1 /\\ f = a /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-8) = i S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, f, g, h, i, f, k, l) [ a >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ c >= j + 1 /\\ f = a /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-9) = a + 1 S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, f, g, h, i, f, k, l) [ a >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ c >= j + 1 /\\ f = a /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-10) = k S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, f, g, h, i, f, k, l) [ a >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ c >= j + 1 /\\ f = a /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-11) = a S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, f + 1, g, h, i, j, k, l) [ a >= f + 1 /\\ f >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ a >= f /\\ c >= j + 1 /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-0) = a S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, f + 1, g, h, i, j, k, l) [ a >= f + 1 /\\ f >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ a >= f /\\ c >= j + 1 /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-1) = c S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, f + 1, g, h, i, j, k, l) [ a >= f + 1 /\\ f >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ a >= f /\\ c >= j + 1 /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-2) = c S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, f + 1, g, h, i, j, k, l) [ a >= f + 1 /\\ f >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ a >= f /\\ c >= j + 1 /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-3) = e S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, f + 1, g, h, i, j, k, l) [ a >= f + 1 /\\ f >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ a >= f /\\ c >= j + 1 /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-4) = e S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, f + 1, g, h, i, j, k, l) [ a >= f + 1 /\\ f >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ a >= f /\\ c >= j + 1 /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-5) = a S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, f + 1, g, h, i, j, k, l) [ a >= f + 1 /\\ f >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ a >= f /\\ c >= j + 1 /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-6) = g S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, f + 1, g, h, i, j, k, l) [ a >= f + 1 /\\ f >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ a >= f /\\ c >= j + 1 /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-7) = 1 S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, f + 1, g, h, i, j, k, l) [ a >= f + 1 /\\ f >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ a >= f /\\ c >= j + 1 /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-8) = i S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, f + 1, g, h, i, j, k, l) [ a >= f + 1 /\\ f >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ a >= f /\\ c >= j + 1 /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-9) = 0 S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, f + 1, g, h, i, j, k, l) [ a >= f + 1 /\\ f >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ a >= f /\\ c >= j + 1 /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-10) = k S("lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, f + 1, g, h, i, j, k, l) [ a >= f + 1 /\\ f >= j + 1 /\\ e >= 1 /\\ j >= 0 /\\ a >= f /\\ c >= j + 1 /\\ h = 1 /\\ l = a /\\ d = e /\\ b = c ]", 0-11) = a S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, 1, i, j, k, l) [ e >= 1 /\\ c >= j + 1 /\\ j >= a /\\ e >= 0 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = e /\\ l = a /\\ d = e /\\ b = c ]", 0-0) = a S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, 1, i, j, k, l) [ e >= 1 /\\ c >= j + 1 /\\ j >= a /\\ e >= 0 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = e /\\ l = a /\\ d = e /\\ b = c ]", 0-1) = c S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, 1, i, j, k, l) [ e >= 1 /\\ c >= j + 1 /\\ j >= a /\\ e >= 0 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = e /\\ l = a /\\ d = e /\\ b = c ]", 0-2) = c S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, 1, i, j, k, l) [ e >= 1 /\\ c >= j + 1 /\\ j >= a /\\ e >= 0 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = e /\\ l = a /\\ d = e /\\ b = c ]", 0-3) = e S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, 1, i, j, k, l) [ e >= 1 /\\ c >= j + 1 /\\ j >= a /\\ e >= 0 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = e /\\ l = a /\\ d = e /\\ b = c ]", 0-4) = e S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, 1, i, j, k, l) [ e >= 1 /\\ c >= j + 1 /\\ j >= a /\\ e >= 0 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = e /\\ l = a /\\ d = e /\\ b = c ]", 0-5) = 3*a + 3*c + 27 S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, 1, i, j, k, l) [ e >= 1 /\\ c >= j + 1 /\\ j >= a /\\ e >= 0 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = e /\\ l = a /\\ d = e /\\ b = c ]", 0-6) = g S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, 1, i, j, k, l) [ e >= 1 /\\ c >= j + 1 /\\ j >= a /\\ e >= 0 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = e /\\ l = a /\\ d = e /\\ b = c ]", 0-7) = 1 S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, 1, i, j, k, l) [ e >= 1 /\\ c >= j + 1 /\\ j >= a /\\ e >= 0 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = e /\\ l = a /\\ d = e /\\ b = c ]", 0-8) = i S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, 1, i, j, k, l) [ e >= 1 /\\ c >= j + 1 /\\ j >= a /\\ e >= 0 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = e /\\ l = a /\\ d = e /\\ b = c ]", 0-9) = 3*a + 3*c + 9 S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, 1, i, j, k, l) [ e >= 1 /\\ c >= j + 1 /\\ j >= a /\\ e >= 0 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = e /\\ l = a /\\ d = e /\\ b = c ]", 0-10) = k S("lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, 1, i, j, k, l) [ e >= 1 /\\ c >= j + 1 /\\ j >= a /\\ e >= 0 /\\ a >= 0 /\\ c >= 1 /\\ a + c >= j /\\ j >= 1 /\\ h = e /\\ l = a /\\ d = e /\\ b = c ]", 0-11) = a orients the transition lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, h + 1, i, j, k, l) [ e >= h + 1 /\ f >= a /\ a + c >= f + 1 /\ a >= 0 /\ e >= h /\ h >= 1 /\ j = f /\ l = a /\ d = e /\ b = c ] weakly and the transition lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, h + 1, i, j, k, l) [ e >= h + 1 /\ f >= a /\ a + c >= f + 1 /\ a >= 0 /\ e >= h /\ h >= 1 /\ j = f /\ l = a /\ d = e /\ b = c ] strictly and produces the following problem: 8: T: (2*a + 2*c, 1) lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, 1, i, j, k, l) [ e >= 1 /\ c >= j + 1 /\ j >= a /\ e >= 0 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = e /\ l = a /\ d = e /\ b = c ] (2*a + 2*c, 1) lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, f + 1, g, h, i, j, k, l) [ a >= f + 1 /\ f >= j + 1 /\ e >= 1 /\ j >= 0 /\ a >= f /\ c >= j + 1 /\ h = 1 /\ l = a /\ d = e /\ b = c ] (5, 1) lbl111(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, f, g, h, i, f, k, l) [ a >= j + 1 /\ e >= 1 /\ j >= 0 /\ c >= j + 1 /\ f = a /\ h = 1 /\ l = a /\ d = e /\ b = c ] (6*e + 2*a*e + 2*c*e + 4*a + 4*c + 12, 1) lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, j, g, h + 1, i, j, k, l) [ e >= h + 1 /\ f >= a /\ a + c >= f + 1 /\ a >= 0 /\ e >= h /\ h >= 1 /\ j = f /\ l = a /\ d = e /\ b = c ] (2*a + 2*c, 1) lbl121(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, h, i, j + 1, k, l) [ a + c >= f + 1 /\ a >= 0 /\ f >= a /\ e >= 1 /\ h = e /\ j = f /\ l = a /\ d = e /\ b = c ] (2*a + 2*c, 1) lbl131(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, j + 1, k, l) [ c >= j + 1 /\ a >= 0 /\ c >= 1 /\ a + c >= j /\ j >= 1 /\ h = 0 /\ d = 0 /\ l = a /\ e = 0 /\ b = c ] (1, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl111(a, b, c, d, e, 1, g, 1, i, 0, k, l) [ a >= 1 /\ e >= 1 /\ c >= 1 /\ b = c /\ d = e /\ f = g /\ h = i /\ j = k /\ l = a ] (1, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl121(a, b, c, d, e, 0, g, 1, i, 0, k, l) [ e >= 1 /\ c >= 1 /\ l = 0 /\ b = c /\ d = e /\ f = g /\ h = i /\ j = k /\ a = 0 ] (1, 1) start(a, b, c, d, e, f, g, h, i, j, k, l) -> lbl131(a, b, c, d, e, f, g, 0, i, 1, k, l) [ a >= 0 /\ c >= 1 /\ d = 0 /\ b = c /\ e = 0 /\ f = g /\ h = i /\ j = k /\ l = a ] (1, 1) start0(a, b, c, d, e, f, g, h, i, j, k, l) -> start(a, c, c, e, e, g, g, i, i, k, k, a) start location: start0 leaf cost: 5 Complexity upper bound 12*a + 12*c + 6*e + 2*a*e + 2*c*e + 26 Time: 1.121 sec (SMT: 1.006 sec)