YES(?, 264*l + 105*l^2 + 12*l^3 + 146)

Initial complexity problem:
1:	T:
		(?, 1)    start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\ c = d /\ e = f /\ g = h /\ i = j /\ k = l /\ m = n /\ o = p ]
		(?, 1)    lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\ 2*a + 1 >= g /\ 2*o + 1 >= l /\ o >= g /\ e >= 0 /\ g >= 1 /\ l >= e + 1 /\ k = l /\ i = l /\ m + 1 = l ]
		(?, 1)    lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> stop(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ e >= 0 /\ 2*o + 1 >= l /\ o >= 1 /\ l >= e + 1 /\ o >= 0 /\ g = 0 /\ k = l /\ i = l /\ m + 1 = l /\ a = 0 ]
		(?, 1)    lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, 0, j, k, l, m, n, o, p) [ a >= 1 /\ 0 >= l /\ a >= 0 /\ e >= 0 /\ 2*o + 1 >= l /\ o >= 1 /\ l >= e + 1 /\ o >= 2*a /\ k = l /\ i = l /\ m + 1 = l /\ g = a ]
		(?, 1)    lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\ a >= 1 /\ a >= 0 /\ e >= 0 /\ 2*o + 1 >= l /\ o >= 1 /\ l >= e + 1 /\ o >= 2*a /\ k = l /\ i = l /\ m + 1 = l /\ g = a ]
		(?, 1)    lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\ i >= g + e /\ o >= g /\ l >= i + 1 /\ g >= 1 /\ 2*o + 1 >= l /\ e >= 0 /\ k = l ]
		(?, 1)    lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\ o >= g /\ l >= i + 1 /\ g >= 1 /\ 2*o + 1 >= l /\ e >= 0 /\ k = l ]
		(?, 1)    lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\ 2*o + 1 >= l /\ o >= g /\ g >= 1 /\ e >= 0 /\ l >= e + 1 /\ i = e /\ k = l ]
		(?, 1)    lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\ o >= g /\ g >= 1 /\ e >= 0 /\ l >= e + 1 /\ i = e /\ k = l ]
		(?, 1)    lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\ g >= 1 /\ e >= 0 /\ o >= g /\ 2*o + 1 >= l /\ i = l /\ k = l /\ m + 1 = l ]
		(?, 1)    lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\ l >= m + 1 /\ m >= e /\ g >= 1 /\ e >= 0 /\ o >= g /\ 2*o + 1 >= l /\ i = m + 1 /\ k = l ]
		(?, 1)    lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> stop(a, b, c, d, e, f, o, h, i, j, k, l, m, n, o, p) [ l >= 2*o /\ 0 >= o /\ 2*o + 1 >= l /\ m = n /\ a = b /\ c = d /\ e = f /\ g = h /\ i = j /\ k = l ]
		(?, 1)    lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\ o >= 1 /\ 2*o + 1 >= l /\ m = n /\ a = b /\ c = d /\ e = f /\ g = h /\ i = j /\ k = l ]
		(1, 1)    start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)
	start location:	start0
	leaf cost:	0

Testing for unsatisfiable constraints removes the following transition from problem 1:
	lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, 0, j, k, l, m, n, o, p) [ a >= 1 /\ 0 >= l /\ a >= 0 /\ e >= 0 /\ 2*o + 1 >= l /\ o >= 1 /\ l >= e + 1 /\ o >= 2*a /\ k = l /\ i = l /\ m + 1 = l /\ g = a ]
We thus obtain the following problem:
2:	T:
		(?, 1)    start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\ c = d /\ e = f /\ g = h /\ i = j /\ k = l /\ m = n /\ o = p ]
		(?, 1)    lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\ 2*a + 1 >= g /\ 2*o + 1 >= l /\ o >= g /\ e >= 0 /\ g >= 1 /\ l >= e + 1 /\ k = l /\ i = l /\ m + 1 = l ]
		(?, 1)    lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> stop(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ e >= 0 /\ 2*o + 1 >= l /\ o >= 1 /\ l >= e + 1 /\ o >= 0 /\ g = 0 /\ k = l /\ i = l /\ m + 1 = l /\ a = 0 ]
		(?, 1)    lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\ a >= 1 /\ a >= 0 /\ e >= 0 /\ 2*o + 1 >= l /\ o >= 1 /\ l >= e + 1 /\ o >= 2*a /\ k = l /\ i = l /\ m + 1 = l /\ g = a ]
		(?, 1)    lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\ i >= g + e /\ o >= g /\ l >= i + 1 /\ g >= 1 /\ 2*o + 1 >= l /\ e >= 0 /\ k = l ]
		(?, 1)    lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\ o >= g /\ l >= i + 1 /\ g >= 1 /\ 2*o + 1 >= l /\ e >= 0 /\ k = l ]
		(?, 1)    lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\ 2*o + 1 >= l /\ o >= g /\ g >= 1 /\ e >= 0 /\ l >= e + 1 /\ i = e /\ k = l ]
		(?, 1)    lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\ o >= g /\ g >= 1 /\ e >= 0 /\ l >= e + 1 /\ i = e /\ k = l ]
		(?, 1)    lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\ g >= 1 /\ e >= 0 /\ o >= g /\ 2*o + 1 >= l /\ i = l /\ k = l /\ m + 1 = l ]
		(?, 1)    lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\ l >= m + 1 /\ m >= e /\ g >= 1 /\ e >= 0 /\ o >= g /\ 2*o + 1 >= l /\ i = m + 1 /\ k = l ]
		(?, 1)    lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> stop(a, b, c, d, e, f, o, h, i, j, k, l, m, n, o, p) [ l >= 2*o /\ 0 >= o /\ 2*o + 1 >= l /\ m = n /\ a = b /\ c = d /\ e = f /\ g = h /\ i = j /\ k = l ]
		(?, 1)    lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\ o >= 1 /\ 2*o + 1 >= l /\ m = n /\ a = b /\ c = d /\ e = f /\ g = h /\ i = j /\ k = l ]
		(1, 1)    start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)
	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, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\ c = d /\ e = f /\ g = h /\ i = j /\ k = l /\ m = n /\ o = p ]
		(?, 1)    lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\ 2*a + 1 >= g /\ 2*o + 1 >= l /\ o >= g /\ e >= 0 /\ g >= 1 /\ l >= e + 1 /\ k = l /\ i = l /\ m + 1 = l ]
		(?, 1)    lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\ a >= 1 /\ a >= 0 /\ e >= 0 /\ 2*o + 1 >= l /\ o >= 1 /\ l >= e + 1 /\ o >= 2*a /\ k = l /\ i = l /\ m + 1 = l /\ g = a ]
		(?, 1)    lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\ i >= g + e /\ o >= g /\ l >= i + 1 /\ g >= 1 /\ 2*o + 1 >= l /\ e >= 0 /\ k = l ]
		(?, 1)    lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\ o >= g /\ l >= i + 1 /\ g >= 1 /\ 2*o + 1 >= l /\ e >= 0 /\ k = l ]
		(?, 1)    lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\ 2*o + 1 >= l /\ o >= g /\ g >= 1 /\ e >= 0 /\ l >= e + 1 /\ i = e /\ k = l ]
		(?, 1)    lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\ o >= g /\ g >= 1 /\ e >= 0 /\ l >= e + 1 /\ i = e /\ k = l ]
		(?, 1)    lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\ g >= 1 /\ e >= 0 /\ o >= g /\ 2*o + 1 >= l /\ i = l /\ k = l /\ m + 1 = l ]
		(?, 1)    lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\ l >= m + 1 /\ m >= e /\ g >= 1 /\ e >= 0 /\ o >= g /\ 2*o + 1 >= l /\ i = m + 1 /\ k = l ]
		(?, 1)    lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\ o >= 1 /\ 2*o + 1 >= l /\ m = n /\ a = b /\ c = d /\ e = f /\ g = h /\ i = j /\ k = l ]
		(1, 1)    start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)
	start location:	start0
	leaf cost:	2

Repeatedly propagating knowledge in problem 3 produces the following problem:
4:	T:
		(1, 1)    start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\ c = d /\ e = f /\ g = h /\ i = j /\ k = l /\ m = n /\ o = p ]
		(?, 1)    lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\ 2*a + 1 >= g /\ 2*o + 1 >= l /\ o >= g /\ e >= 0 /\ g >= 1 /\ l >= e + 1 /\ k = l /\ i = l /\ m + 1 = l ]
		(?, 1)    lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\ a >= 1 /\ a >= 0 /\ e >= 0 /\ 2*o + 1 >= l /\ o >= 1 /\ l >= e + 1 /\ o >= 2*a /\ k = l /\ i = l /\ m + 1 = l /\ g = a ]
		(?, 1)    lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\ i >= g + e /\ o >= g /\ l >= i + 1 /\ g >= 1 /\ 2*o + 1 >= l /\ e >= 0 /\ k = l ]
		(?, 1)    lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\ o >= g /\ l >= i + 1 /\ g >= 1 /\ 2*o + 1 >= l /\ e >= 0 /\ k = l ]
		(?, 1)    lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\ 2*o + 1 >= l /\ o >= g /\ g >= 1 /\ e >= 0 /\ l >= e + 1 /\ i = e /\ k = l ]
		(?, 1)    lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\ o >= g /\ g >= 1 /\ e >= 0 /\ l >= e + 1 /\ i = e /\ k = l ]
		(?, 1)    lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\ g >= 1 /\ e >= 0 /\ o >= g /\ 2*o + 1 >= l /\ i = l /\ k = l /\ m + 1 = l ]
		(?, 1)    lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\ l >= m + 1 /\ m >= e /\ g >= 1 /\ e >= 0 /\ o >= g /\ 2*o + 1 >= l /\ i = m + 1 /\ k = l ]
		(1, 1)    lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\ o >= 1 /\ 2*o + 1 >= l /\ m = n /\ a = b /\ c = d /\ e = f /\ g = h /\ i = j /\ k = l ]
		(1, 1)    start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)
	start location:	start0
	leaf cost:	2

A polynomial rank function with
	Pol(start) = V_11 + 3*V_12 + 2
	Pol(lbl21) = V_11 + 3*V_12 + 2
	Pol(lbl121) = 3*V_7 + V_11 + 4
	Pol(lbl123) = 6*V_1 + V_11 + 3
	Pol(lbl71) = 6*V_7 + V_11 + 2
	Pol(lbl101) = 6*V_7 + V_11 + 2
	Pol(lbl53) = 6*V_7 + V_11 + 2
	Pol(start0) = 4*V_12 + 2
orients all transitions weakly and the transitions
	lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\ g >= 1 /\ e >= 0 /\ o >= g /\ 2*o + 1 >= l /\ i = l /\ k = l /\ m + 1 = l ]
	lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\ a >= 1 /\ a >= 0 /\ e >= 0 /\ 2*o + 1 >= l /\ o >= 1 /\ l >= e + 1 /\ o >= 2*a /\ k = l /\ i = l /\ m + 1 = l /\ g = a ]
	lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\ 2*a + 1 >= g /\ 2*o + 1 >= l /\ o >= g /\ e >= 0 /\ g >= 1 /\ l >= e + 1 /\ k = l /\ i = l /\ m + 1 = l ]
strictly and produces the following problem:
5:	T:
		(1, 1)          start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\ c = d /\ e = f /\ g = h /\ i = j /\ k = l /\ m = n /\ o = p ]
		(4*l + 2, 1)    lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\ 2*a + 1 >= g /\ 2*o + 1 >= l /\ o >= g /\ e >= 0 /\ g >= 1 /\ l >= e + 1 /\ k = l /\ i = l /\ m + 1 = l ]
		(4*l + 2, 1)    lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\ a >= 1 /\ a >= 0 /\ e >= 0 /\ 2*o + 1 >= l /\ o >= 1 /\ l >= e + 1 /\ o >= 2*a /\ k = l /\ i = l /\ m + 1 = l /\ g = a ]
		(?, 1)          lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\ i >= g + e /\ o >= g /\ l >= i + 1 /\ g >= 1 /\ 2*o + 1 >= l /\ e >= 0 /\ k = l ]
		(?, 1)          lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\ o >= g /\ l >= i + 1 /\ g >= 1 /\ 2*o + 1 >= l /\ e >= 0 /\ k = l ]
		(?, 1)          lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\ 2*o + 1 >= l /\ o >= g /\ g >= 1 /\ e >= 0 /\ l >= e + 1 /\ i = e /\ k = l ]
		(?, 1)          lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\ o >= g /\ g >= 1 /\ e >= 0 /\ l >= e + 1 /\ i = e /\ k = l ]
		(4*l + 2, 1)    lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\ g >= 1 /\ e >= 0 /\ o >= g /\ 2*o + 1 >= l /\ i = l /\ k = l /\ m + 1 = l ]
		(?, 1)          lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\ l >= m + 1 /\ m >= e /\ g >= 1 /\ e >= 0 /\ o >= g /\ 2*o + 1 >= l /\ i = m + 1 /\ k = l ]
		(1, 1)          lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\ o >= 1 /\ 2*o + 1 >= l /\ m = n /\ a = b /\ c = d /\ e = f /\ g = h /\ i = j /\ k = l ]
		(1, 1)          start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)
	start location:	start0
	leaf cost:	2

A polynomial rank function with
	Pol(lbl71) = -3*V_9 + 3*V_12 + 9
	Pol(lbl53) = 3*V_12 - 3*V_13 + 7
	Pol(lbl101) = -3*V_9 + 3*V_12 + 8
and size complexities
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-0) = b
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-1) = b
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-2) = d
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-3) = d
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-4) = f
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-5) = f
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-6) = h
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-7) = h
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-8) = j
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-9) = j
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-10) = l
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-11) = l
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-12) = n
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-13) = n
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-14) = p
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-15) = p
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-0) = b
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-1) = b
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-2) = ?
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-3) = d
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-4) = 0
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-5) = f
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-6) = ?
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-7) = h
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-8) = 0
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-9) = j
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-10) = l
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-11) = l
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-12) = n
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-13) = n
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-14) = ?
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-15) = p
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-0) = ?
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-1) = b
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-2) = ?
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-3) = d
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-4) = l
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-5) = f
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-6) = ?
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-7) = h
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-8) = l
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-9) = j
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-10) = l
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-11) = l
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-12) = l
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-13) = n
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-14) = ?
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-15) = p
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-0) = ?
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-1) = b
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-2) = ?
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-3) = d
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-4) = l
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-5) = f
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-6) = ?
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-7) = h
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-8) = l
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-9) = j
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-10) = l
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-11) = l
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-12) = l
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-13) = n
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-14) = ?
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-15) = p
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-0) = ?
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-1) = b
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-2) = ?
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-3) = d
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-4) = l
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-5) = f
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-6) = ?
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-7) = h
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-8) = l
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-9) = j
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-10) = l
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-11) = l
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-12) = l
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-13) = n
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-14) = ?
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-15) = p
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-0) = ?
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-1) = b
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-2) = ?
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-3) = d
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-4) = l
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-5) = f
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-6) = ?
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-7) = h
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-8) = l
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-9) = j
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-10) = l
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-11) = l
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-12) = l
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-13) = n
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-14) = ?
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-15) = p
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-0) = ?
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-1) = b
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-2) = ?
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-3) = d
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-4) = l
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-5) = f
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-6) = ?
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-7) = h
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-8) = l
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-9) = j
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-10) = l
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-11) = l
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-12) = l
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-13) = n
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-14) = ?
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-15) = p
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-0) = ?
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-1) = b
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-2) = ?
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-3) = d
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-4) = l
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-5) = f
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-6) = ?
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-7) = h
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-8) = l
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-9) = j
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-10) = l
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-11) = l
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-12) = l
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-13) = n
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-14) = ?
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-15) = p
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-0) = ?
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-1) = b
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-2) = ?
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-3) = d
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-4) = 0
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-5) = f
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-6) = ?
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-7) = h
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-8) = 0
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-9) = j
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-10) = l
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-11) = l
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-12) = l
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-13) = n
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-14) = ?
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-15) = p
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-0) = ?
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-1) = b
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-2) = ?
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-3) = d
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-4) = l
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-5) = f
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-6) = ?
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-7) = h
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-8) = l
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-9) = j
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-10) = l
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-11) = l
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-12) = l
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-13) = n
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-14) = ?
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-15) = p
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-0) = b
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-1) = b
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-2) = d
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-3) = d
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-4) = f
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-5) = f
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-6) = h
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-7) = h
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-8) = j
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-9) = j
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-10) = l
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-11) = l
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-12) = n
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-13) = n
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-14) = ?
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-15) = p
orients the transitions
	lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\ o >= g /\ g >= 1 /\ e >= 0 /\ l >= e + 1 /\ i = e /\ k = l ]
	lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\ 2*o + 1 >= l /\ o >= g /\ g >= 1 /\ e >= 0 /\ l >= e + 1 /\ i = e /\ k = l ]
	lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\ l >= m + 1 /\ m >= e /\ g >= 1 /\ e >= 0 /\ o >= g /\ 2*o + 1 >= l /\ i = m + 1 /\ k = l ]
	lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\ o >= g /\ l >= i + 1 /\ g >= 1 /\ 2*o + 1 >= l /\ e >= 0 /\ k = l ]
	lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\ i >= g + e /\ o >= g /\ l >= i + 1 /\ g >= 1 /\ 2*o + 1 >= l /\ e >= 0 /\ k = l ]
weakly and the transitions
	lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\ o >= g /\ g >= 1 /\ e >= 0 /\ l >= e + 1 /\ i = e /\ k = l ]
	lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\ 2*o + 1 >= l /\ o >= g /\ g >= 1 /\ e >= 0 /\ l >= e + 1 /\ i = e /\ k = l ]
	lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\ l >= m + 1 /\ m >= e /\ g >= 1 /\ e >= 0 /\ o >= g /\ 2*o + 1 >= l /\ i = m + 1 /\ k = l ]
	lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\ o >= g /\ l >= i + 1 /\ g >= 1 /\ 2*o + 1 >= l /\ e >= 0 /\ k = l ]
strictly and produces the following problem:
6:	T:
		(1, 1)                     start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\ c = d /\ e = f /\ g = h /\ i = j /\ k = l /\ m = n /\ o = p ]
		(4*l + 2, 1)               lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\ 2*a + 1 >= g /\ 2*o + 1 >= l /\ o >= g /\ e >= 0 /\ g >= 1 /\ l >= e + 1 /\ k = l /\ i = l /\ m + 1 = l ]
		(4*l + 2, 1)               lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\ a >= 1 /\ a >= 0 /\ e >= 0 /\ 2*o + 1 >= l /\ o >= 1 /\ l >= e + 1 /\ o >= 2*a /\ k = l /\ i = l /\ m + 1 = l /\ g = a ]
		(?, 1)                     lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\ i >= g + e /\ o >= g /\ l >= i + 1 /\ g >= 1 /\ 2*o + 1 >= l /\ e >= 0 /\ k = l ]
		(45*l + 12*l^2 + 27, 1)    lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\ o >= g /\ l >= i + 1 /\ g >= 1 /\ 2*o + 1 >= l /\ e >= 0 /\ k = l ]
		(45*l + 12*l^2 + 27, 1)    lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\ 2*o + 1 >= l /\ o >= g /\ g >= 1 /\ e >= 0 /\ l >= e + 1 /\ i = e /\ k = l ]
		(45*l + 12*l^2 + 27, 1)    lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\ o >= g /\ g >= 1 /\ e >= 0 /\ l >= e + 1 /\ i = e /\ k = l ]
		(4*l + 2, 1)               lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\ g >= 1 /\ e >= 0 /\ o >= g /\ 2*o + 1 >= l /\ i = l /\ k = l /\ m + 1 = l ]
		(45*l + 12*l^2 + 27, 1)    lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\ l >= m + 1 /\ m >= e /\ g >= 1 /\ e >= 0 /\ o >= g /\ 2*o + 1 >= l /\ i = m + 1 /\ k = l ]
		(1, 1)                     lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\ o >= 1 /\ 2*o + 1 >= l /\ m = n /\ a = b /\ c = d /\ e = f /\ g = h /\ i = j /\ k = l ]
		(1, 1)                     start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)
	start location:	start0
	leaf cost:	2

A polynomial rank function with
	Pol(lbl101) = V_5 + 1
and size complexities
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-0) = b
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-1) = b
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-2) = d
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-3) = d
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-4) = f
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-5) = f
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-6) = h
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-7) = h
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-8) = j
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-9) = j
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-10) = l
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-11) = l
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-12) = n
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-13) = n
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-14) = p
	S("start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)", 0-15) = p
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-0) = b
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-1) = b
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-2) = ?
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-3) = d
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-4) = 0
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-5) = f
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-6) = ?
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-7) = h
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-8) = 0
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-9) = j
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-10) = l
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-11) = l
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-12) = n
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-13) = n
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-14) = ?
	S("lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\\ o >= 1 /\\ 2*o + 1 >= l /\\ m = n /\\ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l ]", 0-15) = p
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-0) = ?
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-1) = b
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-2) = ?
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-3) = d
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-4) = l
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-5) = f
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-6) = ?
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-7) = h
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-8) = l
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-9) = j
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-10) = l
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-11) = l
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-12) = l
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-13) = n
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-14) = ?
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\\ l >= m + 1 /\\ m >= e /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = m + 1 /\\ k = l ]", 0-15) = p
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-0) = ?
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-1) = b
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-2) = ?
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-3) = d
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-4) = l
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-5) = f
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-6) = ?
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-7) = h
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-8) = l
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-9) = j
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-10) = l
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-11) = l
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-12) = l
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-13) = n
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-14) = ?
	S("lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\\ g >= 1 /\\ e >= 0 /\\ o >= g /\\ 2*o + 1 >= l /\\ i = l /\\ k = l /\\ m + 1 = l ]", 0-15) = p
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-0) = ?
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-1) = b
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-2) = ?
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-3) = d
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-4) = l
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-5) = f
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-6) = ?
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-7) = h
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-8) = l
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-9) = j
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-10) = l
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-11) = l
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-12) = l
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-13) = n
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-14) = ?
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-15) = p
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-0) = ?
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-1) = b
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-2) = ?
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-3) = d
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-4) = l
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-5) = f
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-6) = ?
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-7) = h
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-8) = l
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-9) = j
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-10) = l
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-11) = l
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-12) = l
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-13) = n
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-14) = ?
	S("lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ g >= 1 /\\ e >= 0 /\\ l >= e + 1 /\\ i = e /\\ k = l ]", 0-15) = p
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-0) = ?
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-1) = b
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-2) = ?
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-3) = d
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-4) = l
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-5) = f
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-6) = ?
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-7) = h
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-8) = l
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-9) = j
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-10) = l
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-11) = l
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-12) = l
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-13) = n
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-14) = ?
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-15) = p
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-0) = ?
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-1) = b
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-2) = ?
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-3) = d
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-4) = l
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-5) = f
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-6) = ?
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-7) = h
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-8) = l
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-9) = j
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-10) = l
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-11) = l
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-12) = l
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-13) = n
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-14) = ?
	S("lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\\ i >= g + e /\\ o >= g /\\ l >= i + 1 /\\ g >= 1 /\\ 2*o + 1 >= l /\\ e >= 0 /\\ k = l ]", 0-15) = p
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-0) = ?
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-1) = b
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-2) = ?
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-3) = d
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-4) = 0
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-5) = f
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-6) = ?
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-7) = h
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-8) = 0
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-9) = j
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-10) = l
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-11) = l
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-12) = l
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-13) = n
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-14) = ?
	S("lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\\ a >= 1 /\\ a >= 0 /\\ e >= 0 /\\ 2*o + 1 >= l /\\ o >= 1 /\\ l >= e + 1 /\\ o >= 2*a /\\ k = l /\\ i = l /\\ m + 1 = l /\\ g = a ]", 0-15) = p
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-0) = ?
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-1) = b
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-2) = ?
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-3) = d
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-4) = l
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-5) = f
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-6) = ?
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-7) = h
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-8) = l
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-9) = j
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-10) = l
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-11) = l
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-12) = l
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-13) = n
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-14) = ?
	S("lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\\ 2*a + 1 >= g /\\ 2*o + 1 >= l /\\ o >= g /\\ e >= 0 /\\ g >= 1 /\\ l >= e + 1 /\\ k = l /\\ i = l /\\ m + 1 = l ]", 0-15) = p
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-0) = b
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-1) = b
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-2) = d
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-3) = d
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-4) = f
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-5) = f
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-6) = h
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-7) = h
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-8) = j
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-9) = j
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-10) = l
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-11) = l
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-12) = n
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-13) = n
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-14) = ?
	S("start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\\ c = d /\\ e = f /\\ g = h /\\ i = j /\\ k = l /\\ m = n /\\ o = p ]", 0-15) = p
orients the transition
	lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\ i >= g + e /\ o >= g /\ l >= i + 1 /\ g >= 1 /\ 2*o + 1 >= l /\ e >= 0 /\ k = l ]
weakly and the transition
	lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\ i >= g + e /\ o >= g /\ l >= i + 1 /\ g >= 1 /\ 2*o + 1 >= l /\ e >= 0 /\ k = l ]
strictly and produces the following problem:
7:	T:
		(1, 1)                              start(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, q, p) [ a = b /\ c = d /\ e = f /\ g = h /\ i = j /\ k = l /\ m = n /\ o = p ]
		(4*l + 2, 1)                        lbl121(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl123(a, b, c, d, e, f, a, h, i, j, k, l, m, n, o, p) [ g >= 2*a /\ 2*a + 1 >= g /\ 2*o + 1 >= l /\ o >= g /\ e >= 0 /\ g >= 1 /\ l >= e + 1 /\ k = l /\ i = l /\ m + 1 = l ]
		(4*l + 2, 1)                        lbl123(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, g, h, 0, j, k, l, m, n, o, p) [ l >= 1 /\ a >= 1 /\ a >= 0 /\ e >= 0 /\ 2*o + 1 >= l /\ o >= 1 /\ l >= e + 1 /\ o >= 2*a /\ k = l /\ i = l /\ m + 1 = l /\ g = a ]
		(57*l^2 + 12*l^3 + 72*l + 27, 1)    lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\ i >= g + e /\ o >= g /\ l >= i + 1 /\ g >= 1 /\ 2*o + 1 >= l /\ e >= 0 /\ k = l ]
		(45*l + 12*l^2 + 27, 1)             lbl101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ i >= g + e /\ o >= g /\ l >= i + 1 /\ g >= 1 /\ 2*o + 1 >= l /\ e >= 0 /\ k = l ]
		(45*l + 12*l^2 + 27, 1)             lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl101(a, b, c, d, e - g, f, g, h, i, j, k, l, m, n, o, p) [ e >= g /\ 2*o + 1 >= l /\ o >= g /\ g >= 1 /\ e >= 0 /\ l >= e + 1 /\ i = e /\ k = l ]
		(45*l + 12*l^2 + 27, 1)             lbl71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl53(a, b, c, d, e, f, g, h, i + 1, j, k, l, i, n, o, p) [ 2*o + 1 >= l /\ o >= g /\ g >= 1 /\ e >= 0 /\ l >= e + 1 /\ i = e /\ k = l ]
		(4*l + 2, 1)                        lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl121(q, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) [ l >= e + 1 /\ g >= 1 /\ e >= 0 /\ o >= g /\ 2*o + 1 >= l /\ i = l /\ k = l /\ m + 1 = l ]
		(45*l + 12*l^2 + 27, 1)             lbl53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, i, f, g, h, i, j, k, l, m, n, o, p) [ l >= m + 2 /\ l >= m + 1 /\ m >= e /\ g >= 1 /\ e >= 0 /\ o >= g /\ 2*o + 1 >= l /\ i = m + 1 /\ k = l ]
		(1, 1)                              lbl21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> lbl71(a, b, q, d, 0, f, o, h, 0, j, k, l, m, n, o, p) [ l >= 2*o /\ o >= 1 /\ 2*o + 1 >= l /\ m = n /\ a = b /\ c = d /\ e = f /\ g = h /\ i = j /\ k = l ]
		(1, 1)                              start0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> start(b, b, d, d, f, f, h, h, j, j, l, l, n, n, p, p)
	start location:	start0
	leaf cost:	2

Complexity upper bound 264*l + 105*l^2 + 12*l^3 + 146

Time: 1.043 sec (SMT: 0.858 sec)