YES(?, 11928) Initial complexity problem: 1: T: (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f17(100, 0, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f17(100, 10, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) (?, 1) f17(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f20(a, b, b, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) [ 0 >= b + 1 ] (?, 1) f17(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f20(a, b, b, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) [ b >= 1 ] (?, 1) f17(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f45(a, 0, 0, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) [ b = 0 ] (?, 1) f20(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f26(a, b, c, 0, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) (?, 1) f20(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f26(a, b, c, 10, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) (?, 1) f26(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f45(a, b, c, 0, 0, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) [ d = 0 ] (?, 1) f26(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f29(a, b, c, d, d, 0, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) [ 0 >= d + 1 ] (?, 1) f26(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f29(a, b, c, d, d, 0, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) [ d >= 1 ] (?, 1) f45(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f57(a, b, c, d, e, f, 200, 0, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) (?, 1) f45(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f57(a, b, c, d, e, f, 200, 10, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) (?, 1) f57(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f60(a, b, c, d, e, f, g, h, h, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) [ 0 >= h + 1 ] (?, 1) f57(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f60(a, b, c, d, e, f, g, h, h, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) [ h >= 1 ] (?, 1) f57(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f85(a, b, c, d, e, f, g, 0, 0, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) [ h = 0 ] (?, 1) f60(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f66(a, b, c, d, e, f, g, h, i, 0, k, l, m, n, o, p, q, r, s, t, u, v, w, x) (?, 1) f60(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f66(a, b, c, d, e, f, g, h, i, 10, k, l, m, n, o, p, q, r, s, t, u, v, w, x) (?, 1) f66(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f85(a, b, c, d, e, f, g, h, i, 0, 0, l, m, n, o, p, q, r, s, t, u, v, w, x) [ j = 0 ] (?, 1) f66(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f69(a, b, c, d, e, f, g, h, i, j, j, 0, m, n, o, p, q, r, s, t, u, v, w, x) [ 0 >= j + 1 ] (?, 1) f66(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f69(a, b, c, d, e, f, g, h, i, j, j, 0, m, n, o, p, q, r, s, t, u, v, w, x) [ j >= 1 ] (?, 1) f85(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f97(a, b, c, d, e, f, g, h, i, j, k, l, 50, 0, o, p, q, r, s, t, u, v, w, x) (?, 1) f85(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f97(a, b, c, d, e, f, g, h, i, j, k, l, 50, 10, o, p, q, r, s, t, u, v, w, x) (?, 1) f97(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f100(a, b, c, d, e, f, g, h, i, j, k, l, m, n, n, p, q, r, s, t, u, v, w, x) [ 0 >= n + 1 ] (?, 1) f97(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f100(a, b, c, d, e, f, g, h, i, j, k, l, m, n, n, p, q, r, s, t, u, v, w, x) [ n >= 1 ] (?, 1) f97(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f125(a, b, c, d, e, f, g, h, i, j, k, l, m, 0, 0, p, q, r, s, t, u, v, w, x) [ n = 0 ] (?, 1) f100(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f106(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, 0, q, r, s, t, u, v, w, x) (?, 1) f100(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f106(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, 10, q, r, s, t, u, v, w, x) (?, 1) f106(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f125(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, 0, 0, r, s, t, u, v, w, x) [ p = 0 ] (?, 1) f106(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f109(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, p, 0, s, t, u, v, w, x) [ 0 >= p + 1 ] (?, 1) f106(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f109(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, p, 0, s, t, u, v, w, x) [ p >= 1 ] (?, 1) f125(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f137(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, 20, 0, u, v, w, x) (?, 1) f125(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f137(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, 20, 10, u, v, w, x) (?, 1) f137(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f140(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, t, v, w, x) [ 0 >= t + 1 ] (?, 1) f137(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f140(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, t, v, w, x) [ t >= 1 ] (?, 1) f140(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f146(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, 0, w, x) (?, 1) f140(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f146(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, 10, w, x) (?, 1) f146(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f149(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, v, 0) [ 0 >= v + 1 ] (?, 1) f146(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f149(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, v, 0) [ v >= 1 ] (?, 1) f137(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f166(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, 0, 0, v, w, x) [ t = 0 ] (?, 1) f146(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f166(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, 0, 0, x) [ v = 0 ] (?, 1) f149(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f149(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x + 1) [ s >= x + 1 ] (?, 1) f149(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f166(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) [ x >= s ] (?, 1) f109(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f109(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r + 1, s, t, u, v, w, x) [ m >= r + 1 ] (?, 1) f109(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f125(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) [ r >= m ] (?, 1) f69(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f69(a, b, c, d, e, f, g, h, i, j, k, l + 1, m, n, o, p, q, r, s, t, u, v, w, x) [ g >= l + 1 ] (?, 1) f69(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f85(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) [ l >= g ] (?, 1) f29(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f29(a, b, c, d, e, f + 1, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) [ a >= f + 1 ] (?, 1) f29(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f45(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) [ f >= a ] start location: f0 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x]. We thus obtain the following problem: 2: T: (?, 1) f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ] (?, 1) f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ] (?, 1) f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ] (?, 1) f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ] (?, 1) f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ] (?, 1) f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ] (?, 1) f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f166(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ x >= s ] (?, 1) f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ] (?, 1) f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f166(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 0, x) [ v = 0 ] (?, 1) f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f166(a, b, d, f, g, h, j, l, m, n, p, r, s, 0, v, x) [ t = 0 ] (?, 1) f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ] (?, 1) f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ 0 >= v + 1 ] (?, 1) f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x) (?, 1) f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 0, x) (?, 1) f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ] (?, 1) f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ 0 >= t + 1 ] (?, 1) f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x) (?, 1) f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 0, v, x) (?, 1) f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ] (?, 1) f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ 0 >= p + 1 ] (?, 1) f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ] (?, 1) f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x) (?, 1) f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) (?, 1) f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ] (?, 1) f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ] (?, 1) f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ 0 >= n + 1 ] (?, 1) f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x) (?, 1) f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x) (?, 1) f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ] (?, 1) f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ 0 >= j + 1 ] (?, 1) f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ] (?, 1) f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x) (?, 1) f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) (?, 1) f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ] (?, 1) f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ] (?, 1) f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ 0 >= h + 1 ] (?, 1) f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x) (?, 1) f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x) (?, 1) f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ d >= 1 ] (?, 1) f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ 0 >= d + 1 ] (?, 1) f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) [ d = 0 ] (?, 1) f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 10, f, g, h, j, l, m, n, p, r, s, t, v, x) (?, 1) f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) (?, 1) f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b = 0 ] (?, 1) f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b >= 1 ] (?, 1) f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ 0 >= b + 1 ] (1, 1) f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 10, d, f, g, h, j, l, m, n, p, r, s, t, v, x) (1, 1) f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (?, 1) f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ] (?, 1) f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ] (?, 1) f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ] (?, 1) f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ] (?, 1) f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ] (?, 1) f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ] (?, 1) f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ] (?, 1) f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ] (?, 1) f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ 0 >= v + 1 ] (?, 1) f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x) (?, 1) f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ] (?, 1) f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ 0 >= t + 1 ] (?, 1) f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x) (?, 1) f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ] (?, 1) f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ 0 >= p + 1 ] (?, 1) f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ] (?, 1) f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x) (?, 1) f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) (?, 1) f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ] (?, 1) f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ] (?, 1) f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ 0 >= n + 1 ] (?, 1) f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x) (?, 1) f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x) (?, 1) f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ] (?, 1) f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ 0 >= j + 1 ] (?, 1) f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ] (?, 1) f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x) (?, 1) f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) (?, 1) f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ] (?, 1) f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ] (?, 1) f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ 0 >= h + 1 ] (?, 1) f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x) (?, 1) f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x) (?, 1) f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ d >= 1 ] (?, 1) f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ 0 >= d + 1 ] (?, 1) f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) [ d = 0 ] (?, 1) f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 10, f, g, h, j, l, m, n, p, r, s, t, v, x) (?, 1) f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) (?, 1) f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b = 0 ] (?, 1) f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b >= 1 ] (?, 1) f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ 0 >= b + 1 ] (1, 1) f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 10, d, f, g, h, j, l, m, n, p, r, s, t, v, x) (1, 1) f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) start location: f0 leaf cost: 5 Testing for reachability in the complexity graph removes the following transitions from problem 3: f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ 0 >= v + 1 ] f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ 0 >= t + 1 ] f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ 0 >= p + 1 ] f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ 0 >= n + 1 ] f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ 0 >= j + 1 ] f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ 0 >= h + 1 ] f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ 0 >= d + 1 ] f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ 0 >= b + 1 ] We thus obtain the following problem: 4: T: (?, 1) f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ] (?, 1) f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ] (?, 1) f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ] (?, 1) f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ] (?, 1) f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x) (?, 1) f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ] (?, 1) f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ] (?, 1) f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ] (?, 1) f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ] (?, 1) f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ] (?, 1) f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) (?, 1) f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x) (?, 1) f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x) (?, 1) f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ] (?, 1) f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ] (?, 1) f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ] (?, 1) f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ] (?, 1) f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ] (?, 1) f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ] (?, 1) f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) (?, 1) f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x) (?, 1) f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x) (?, 1) f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x) (?, 1) f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) [ d = 0 ] (?, 1) f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ d >= 1 ] (?, 1) f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ] (?, 1) f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ] (?, 1) f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) (?, 1) f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 10, f, g, h, j, l, m, n, p, r, s, t, v, x) (?, 1) f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x) (?, 1) f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x) (?, 1) f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b = 0 ] (?, 1) f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b >= 1 ] (1, 1) f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) (1, 1) f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 10, d, f, g, h, j, l, m, n, p, r, s, t, v, x) start location: f0 leaf cost: 5 Repeatedly propagating knowledge in problem 4 produces the following problem: 5: T: (?, 1) f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ] (?, 1) f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ] (?, 1) f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ] (?, 1) f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ] (?, 1) f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x) (?, 1) f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ] (?, 1) f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ] (?, 1) f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ] (?, 1) f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ] (?, 1) f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ] (?, 1) f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) (?, 1) f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x) (?, 1) f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x) (?, 1) f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ] (?, 1) f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ] (?, 1) f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ] (?, 1) f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ] (?, 1) f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ] (?, 1) f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ] (?, 1) f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) (?, 1) f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x) (?, 1) f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x) (?, 1) f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x) (1, 1) f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) [ d = 0 ] (1, 1) f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ d >= 1 ] (?, 1) f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ] (?, 1) f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ] (1, 1) f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) (1, 1) f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 10, f, g, h, j, l, m, n, p, r, s, t, v, x) (?, 1) f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x) (?, 1) f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x) (1, 1) f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b = 0 ] (1, 1) f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b >= 1 ] (1, 1) f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) (1, 1) f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 10, d, f, g, h, j, l, m, n, p, r, s, t, v, x) start location: f0 leaf cost: 5 A polynomial rank function with Pol(f149) = -1 Pol(f146) = 1 Pol(f109) = 5 Pol(f125) = 4 Pol(f140) = 2 Pol(f106) = 6 Pol(f137) = 3 Pol(f69) = 10 Pol(f85) = 9 Pol(f100) = 7 Pol(f66) = 11 Pol(f97) = 8 Pol(f29) = 15 Pol(f45) = 14 Pol(f60) = 12 Pol(f26) = 15 Pol(f57) = 13 Pol(f20) = 15 Pol(f17) = 15 Pol(f0) = 15 orients all transitions weakly and the transitions f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ] f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ] f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x) f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x) f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ] f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ] f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ] f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x) f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ] f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ] f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x) f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x) f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ] f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ] f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x) f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ] f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x) f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ] f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ] f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ] f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x) f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) strictly and produces the following problem: 6: T: (?, 1) f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ] (15, 1) f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ] (?, 1) f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ] (15, 1) f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ] (15, 1) f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x) (15, 1) f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ] (15, 1) f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ] (15, 1) f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ] (?, 1) f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ] (15, 1) f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ] (15, 1) f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) (15, 1) f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x) (15, 1) f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x) (15, 1) f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ] (15, 1) f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ] (15, 1) f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ] (15, 1) f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ] (?, 1) f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ] (15, 1) f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ] (15, 1) f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) (15, 1) f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x) (15, 1) f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x) (15, 1) f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x) (1, 1) f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) [ d = 0 ] (1, 1) f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ d >= 1 ] (15, 1) f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ] (15, 1) f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ] (1, 1) f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) (1, 1) f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 10, f, g, h, j, l, m, n, p, r, s, t, v, x) (15, 1) f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x) (15, 1) f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x) (1, 1) f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b = 0 ] (1, 1) f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b >= 1 ] (1, 1) f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) (1, 1) f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 10, d, f, g, h, j, l, m, n, p, r, s, t, v, x) start location: f0 leaf cost: 5 A polynomial rank function with Pol(f149) = V_13 - V_16 Pol(f146) = V_13 Pol(f109) = 20 Pol(f125) = 20 Pol(f140) = V_13 Pol(f106) = 20 Pol(f137) = V_13 Pol(f69) = 20 Pol(f85) = 20 Pol(f100) = 20 Pol(f66) = 20 Pol(f97) = 20 Pol(f29) = 20 Pol(f45) = 20 Pol(f60) = 20 Pol(f26) = 20 Pol(f57) = 20 Pol(f20) = 20 Pol(f17) = 20 Pol(f0) = 20 orients all transitions weakly and the transition f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ] strictly and produces the following problem: 7: T: (20, 1) f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ] (15, 1) f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ] (?, 1) f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ] (15, 1) f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ] (15, 1) f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x) (15, 1) f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ] (15, 1) f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ] (15, 1) f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ] (?, 1) f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ] (15, 1) f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ] (15, 1) f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) (15, 1) f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x) (15, 1) f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x) (15, 1) f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ] (15, 1) f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ] (15, 1) f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ] (15, 1) f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ] (?, 1) f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ] (15, 1) f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ] (15, 1) f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) (15, 1) f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x) (15, 1) f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x) (15, 1) f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x) (1, 1) f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) [ d = 0 ] (1, 1) f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ d >= 1 ] (15, 1) f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ] (15, 1) f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ] (1, 1) f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) (1, 1) f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 10, f, g, h, j, l, m, n, p, r, s, t, v, x) (15, 1) f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x) (15, 1) f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x) (1, 1) f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b = 0 ] (1, 1) f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b >= 1 ] (1, 1) f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) (1, 1) f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 10, d, f, g, h, j, l, m, n, p, r, s, t, v, x) start location: f0 leaf cost: 5 A polynomial rank function with Pol(f69) = V_5 - V_8 Pol(f29) = V_1 - V_4 Pol(f109) = V_9 - V_12 and size complexities S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 10, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-0) = 100 S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 10, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-1) = 10 S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 10, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-2) = d S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 10, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-3) = f S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 10, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-4) = g S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 10, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-5) = h S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 10, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-6) = j S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 10, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-7) = l S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 10, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-8) = m S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 10, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-9) = n S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 10, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-10) = p S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 10, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-11) = r S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 10, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-12) = s S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 10, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-13) = t S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 10, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-14) = v S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 10, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-15) = x S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-0) = 100 S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-1) = 0 S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-2) = d S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-3) = f S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-4) = g S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-5) = h S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-6) = j S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-7) = l S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-8) = m S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-9) = n S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-10) = p S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-11) = r S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-12) = s S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-13) = t S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-14) = v S("f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-15) = x S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b >= 1 ]", 0-0) = 100 S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b >= 1 ]", 0-1) = 10 S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b >= 1 ]", 0-2) = d S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b >= 1 ]", 0-3) = f S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b >= 1 ]", 0-4) = g S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b >= 1 ]", 0-5) = h S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b >= 1 ]", 0-6) = j S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b >= 1 ]", 0-7) = l S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b >= 1 ]", 0-8) = m S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b >= 1 ]", 0-9) = n S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b >= 1 ]", 0-10) = p S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b >= 1 ]", 0-11) = r S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b >= 1 ]", 0-12) = s S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b >= 1 ]", 0-13) = t S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b >= 1 ]", 0-14) = v S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b >= 1 ]", 0-15) = x S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b = 0 ]", 0-0) = 100 S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b = 0 ]", 0-1) = 0 S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b = 0 ]", 0-2) = d S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b = 0 ]", 0-3) = f S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b = 0 ]", 0-4) = g S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b = 0 ]", 0-5) = h S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b = 0 ]", 0-6) = j S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b = 0 ]", 0-7) = l S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b = 0 ]", 0-8) = m S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b = 0 ]", 0-9) = n S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b = 0 ]", 0-10) = p S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b = 0 ]", 0-11) = r S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b = 0 ]", 0-12) = s S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b = 0 ]", 0-13) = t S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b = 0 ]", 0-14) = v S("f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b = 0 ]", 0-15) = x S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x)", 0-0) = 100 S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x)", 0-1) = 10 S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x)", 0-2) = d + 10 S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x)", 0-3) = ? S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x)", 0-4) = 200 S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x)", 0-5) = 10 S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x)", 0-6) = j S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x)", 0-7) = l S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x)", 0-8) = m S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x)", 0-9) = n S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x)", 0-10) = p S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x)", 0-11) = r S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x)", 0-12) = s S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x)", 0-13) = t S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x)", 0-14) = v S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x)", 0-15) = x S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x)", 0-0) = 100 S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x)", 0-1) = 10 S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x)", 0-2) = d + 10 S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x)", 0-3) = ? S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x)", 0-4) = 200 S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x)", 0-5) = 0 S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x)", 0-6) = j S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x)", 0-7) = l S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x)", 0-8) = m S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x)", 0-9) = n S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x)", 0-10) = p S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x)", 0-11) = r S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x)", 0-12) = s S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x)", 0-13) = t S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x)", 0-14) = v S("f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x)", 0-15) = x S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 10, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-0) = 100 S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 10, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-1) = 10 S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 10, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-2) = 10 S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 10, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-3) = f S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 10, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-4) = g S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 10, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-5) = h S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 10, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-6) = j S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 10, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-7) = l S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 10, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-8) = m S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 10, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-9) = n S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 10, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-10) = p S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 10, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-11) = r S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 10, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-12) = s S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 10, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-13) = t S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 10, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-14) = v S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 10, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-15) = x S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-0) = 100 S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-1) = 10 S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-2) = 0 S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-3) = f S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-4) = g S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-5) = h S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-6) = j S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-7) = l S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-8) = m S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-9) = n S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-10) = p S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-11) = r S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-12) = s S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-13) = t S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-14) = v S("f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x)", 0-15) = x S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ]", 0-0) = 100 S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ]", 0-1) = 10 S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ]", 0-2) = d + 10 S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ]", 0-3) = ? S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ]", 0-4) = 200 S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ]", 0-5) = 10 S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ]", 0-6) = j S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ]", 0-7) = l S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ]", 0-8) = m S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ]", 0-9) = n S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ]", 0-10) = p S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ]", 0-11) = r S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ]", 0-12) = s S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ]", 0-13) = t S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ]", 0-14) = v S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ]", 0-15) = x S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ]", 0-0) = 100 S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ]", 0-1) = 10 S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ]", 0-2) = d + 10 S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ]", 0-3) = ? S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ]", 0-4) = 200 S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ]", 0-5) = 0 S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ]", 0-6) = j S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ]", 0-7) = l S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ]", 0-8) = m S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ]", 0-9) = n S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ]", 0-10) = p S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ]", 0-11) = r S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ]", 0-12) = s S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ]", 0-13) = t S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ]", 0-14) = v S("f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ]", 0-15) = x S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ d >= 1 ]", 0-0) = 100 S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ d >= 1 ]", 0-1) = 10 S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ d >= 1 ]", 0-2) = 10 S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ d >= 1 ]", 0-3) = 0 S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ d >= 1 ]", 0-4) = g S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ d >= 1 ]", 0-5) = h S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ d >= 1 ]", 0-6) = j S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ d >= 1 ]", 0-7) = l S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ d >= 1 ]", 0-8) = m S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ d >= 1 ]", 0-9) = n S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ d >= 1 ]", 0-10) = p S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ d >= 1 ]", 0-11) = r S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ d >= 1 ]", 0-12) = s S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ d >= 1 ]", 0-13) = t S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ d >= 1 ]", 0-14) = v S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ d >= 1 ]", 0-15) = x S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) [ d = 0 ]", 0-0) = 100 S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) [ d = 0 ]", 0-1) = 10 S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) [ d = 0 ]", 0-2) = 0 S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) [ d = 0 ]", 0-3) = f S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) [ d = 0 ]", 0-4) = g S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) [ d = 0 ]", 0-5) = h S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) [ d = 0 ]", 0-6) = j S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) [ d = 0 ]", 0-7) = l S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) [ d = 0 ]", 0-8) = m S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) [ d = 0 ]", 0-9) = n S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) [ d = 0 ]", 0-10) = p S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) [ d = 0 ]", 0-11) = r S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) [ d = 0 ]", 0-12) = s S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) [ d = 0 ]", 0-13) = t S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) [ d = 0 ]", 0-14) = v S("f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) [ d = 0 ]", 0-15) = x S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x)", 0-0) = 100 S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x)", 0-1) = 10 S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x)", 0-2) = d + 10 S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x)", 0-3) = ? S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x)", 0-4) = 200 S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x)", 0-5) = 10 S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x)", 0-6) = j + 10 S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x)", 0-7) = ? S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x)", 0-8) = 50 S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x)", 0-9) = 10 S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x)", 0-10) = p S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x)", 0-11) = r S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x)", 0-12) = s S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x)", 0-13) = t S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x)", 0-14) = v S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x)", 0-15) = x S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x)", 0-0) = 100 S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x)", 0-1) = 10 S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x)", 0-2) = d + 10 S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x)", 0-3) = ? S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x)", 0-4) = 200 S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x)", 0-5) = 10 S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x)", 0-6) = j + 10 S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x)", 0-7) = ? S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x)", 0-8) = 50 S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x)", 0-9) = 0 S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x)", 0-10) = p S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x)", 0-11) = r S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x)", 0-12) = s S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x)", 0-13) = t S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x)", 0-14) = v S("f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x)", 0-15) = x S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x)", 0-0) = 100 S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x)", 0-1) = 10 S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x)", 0-2) = d + 10 S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x)", 0-3) = ? S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x)", 0-4) = 200 S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x)", 0-5) = 10 S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x)", 0-6) = 10 S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x)", 0-7) = l S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x)", 0-8) = m S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x)", 0-9) = n S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x)", 0-10) = p S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x)", 0-11) = r S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x)", 0-12) = s S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x)", 0-13) = t S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x)", 0-14) = v S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x)", 0-15) = x S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x)", 0-0) = 100 S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x)", 0-1) = 10 S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x)", 0-2) = d + 10 S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x)", 0-3) = ? S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x)", 0-4) = 200 S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x)", 0-5) = 10 S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x)", 0-6) = 0 S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x)", 0-7) = l S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x)", 0-8) = m S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x)", 0-9) = n S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x)", 0-10) = p S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x)", 0-11) = r S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x)", 0-12) = s S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x)", 0-13) = t S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x)", 0-14) = v S("f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x)", 0-15) = x S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ]", 0-0) = 100 S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ]", 0-1) = 10 S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ]", 0-2) = 10 S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ]", 0-3) = ? S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ]", 0-4) = g S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ]", 0-5) = h S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ]", 0-6) = j S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ]", 0-7) = l S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ]", 0-8) = m S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ]", 0-9) = n S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ]", 0-10) = p S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ]", 0-11) = r S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ]", 0-12) = s S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ]", 0-13) = t S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ]", 0-14) = v S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ]", 0-15) = x S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ]", 0-0) = 100 S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ]", 0-1) = 10 S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ]", 0-2) = 10 S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ]", 0-3) = ? S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ]", 0-4) = g S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ]", 0-5) = h S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ]", 0-6) = j S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ]", 0-7) = l S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ]", 0-8) = m S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ]", 0-9) = n S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ]", 0-10) = p S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ]", 0-11) = r S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ]", 0-12) = s S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ]", 0-13) = t S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ]", 0-14) = v S("f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ]", 0-15) = x S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ]", 0-0) = 100 S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ]", 0-1) = 10 S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ]", 0-2) = d + 10 S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ]", 0-3) = ? S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ]", 0-4) = 200 S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ]", 0-5) = 10 S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ]", 0-6) = j + 10 S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ]", 0-7) = ? S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ]", 0-8) = 50 S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ]", 0-9) = 10 S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ]", 0-10) = p S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ]", 0-11) = r S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ]", 0-12) = s S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ]", 0-13) = t S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ]", 0-14) = v S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ]", 0-15) = x S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ]", 0-0) = 100 S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ]", 0-1) = 10 S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ]", 0-2) = d + 10 S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ]", 0-3) = ? S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ]", 0-4) = 200 S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ]", 0-5) = 10 S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ]", 0-6) = j + 10 S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ]", 0-7) = ? S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ]", 0-8) = 50 S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ]", 0-9) = 0 S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ]", 0-10) = p S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ]", 0-11) = r S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ]", 0-12) = s S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ]", 0-13) = t S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ]", 0-14) = v S("f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ]", 0-15) = x S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ]", 0-0) = 100 S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ]", 0-1) = 10 S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ]", 0-2) = d + 10 S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ]", 0-3) = ? S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ]", 0-4) = 200 S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ]", 0-5) = 10 S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ]", 0-6) = 10 S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ]", 0-7) = 0 S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ]", 0-8) = m S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ]", 0-9) = n S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ]", 0-10) = p S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ]", 0-11) = r S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ]", 0-12) = s S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ]", 0-13) = t S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ]", 0-14) = v S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ]", 0-15) = x S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ]", 0-0) = 100 S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ]", 0-1) = 10 S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ]", 0-2) = d + 10 S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ]", 0-3) = ? S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ]", 0-4) = 200 S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ]", 0-5) = 10 S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ]", 0-6) = 0 S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ]", 0-7) = l S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ]", 0-8) = m S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ]", 0-9) = n S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ]", 0-10) = p S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ]", 0-11) = r S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ]", 0-12) = s S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ]", 0-13) = t S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ]", 0-14) = v S("f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ]", 0-15) = x S("f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x)", 0-0) = 100 S("f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x)", 0-1) = 10 S("f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x)", 0-2) = d + 10 S("f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x)", 0-3) = ? S("f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x)", 0-4) = 200 S("f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x)", 0-5) = 10 S("f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x)", 0-6) = j + 10 S("f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x)", 0-7) = ? S("f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x)", 0-8) = 50 S("f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x)", 0-9) = 10 S("f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x)", 0-10) = p + 10 S("f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x)", 0-11) = ? S("f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x)", 0-12) = 20 S("f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x)", 0-13) = 10 S("f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x)", 0-14) = v S("f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x)", 0-15) = x S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x)", 0-0) = 100 S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x)", 0-1) = 10 S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x)", 0-2) = d + 10 S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x)", 0-3) = ? S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x)", 0-4) = 200 S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x)", 0-5) = 10 S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x)", 0-6) = j + 10 S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x)", 0-7) = ? S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x)", 0-8) = 50 S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x)", 0-9) = 10 S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x)", 0-10) = 10 S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x)", 0-11) = r S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x)", 0-12) = s S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x)", 0-13) = t S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x)", 0-14) = v S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x)", 0-15) = x S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x)", 0-0) = 100 S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x)", 0-1) = 10 S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x)", 0-2) = d + 10 S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x)", 0-3) = ? S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x)", 0-4) = 200 S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x)", 0-5) = 10 S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x)", 0-6) = j + 10 S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x)", 0-7) = ? S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x)", 0-8) = 50 S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x)", 0-9) = 10 S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x)", 0-10) = 0 S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x)", 0-11) = r S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x)", 0-12) = s S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x)", 0-13) = t S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x)", 0-14) = v S("f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x)", 0-15) = x S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ]", 0-0) = 100 S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ]", 0-1) = 10 S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ]", 0-2) = d + 10 S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ]", 0-3) = ? S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ]", 0-4) = 200 S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ]", 0-5) = 10 S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ]", 0-6) = 10 S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ]", 0-7) = ? S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ]", 0-8) = m S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ]", 0-9) = n S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ]", 0-10) = p S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ]", 0-11) = r S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ]", 0-12) = s S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ]", 0-13) = t S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ]", 0-14) = v S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ]", 0-15) = x S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ]", 0-0) = 100 S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ]", 0-1) = 10 S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ]", 0-2) = d + 10 S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ]", 0-3) = ? S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ]", 0-4) = 200 S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ]", 0-5) = 10 S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ]", 0-6) = 10 S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ]", 0-7) = ? S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ]", 0-8) = m S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ]", 0-9) = n S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ]", 0-10) = p S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ]", 0-11) = r S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ]", 0-12) = s S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ]", 0-13) = t S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ]", 0-14) = v S("f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ]", 0-15) = x S("f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ]", 0-0) = 100 S("f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ]", 0-1) = 10 S("f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ]", 0-2) = d + 10 S("f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ]", 0-3) = ? S("f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ]", 0-4) = 200 S("f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ]", 0-5) = 10 S("f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ]", 0-6) = j + 10 S("f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ]", 0-7) = ? S("f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ]", 0-8) = 50 S("f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ]", 0-9) = 10 S("f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ]", 0-10) = p + 10 S("f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ]", 0-11) = ? S("f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ]", 0-12) = 20 S("f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ]", 0-13) = 10 S("f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ]", 0-14) = v S("f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ]", 0-15) = x S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ]", 0-0) = 100 S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ]", 0-1) = 10 S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ]", 0-2) = d + 10 S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ]", 0-3) = ? S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ]", 0-4) = 200 S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ]", 0-5) = 10 S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ]", 0-6) = j + 10 S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ]", 0-7) = ? S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ]", 0-8) = 50 S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ]", 0-9) = 10 S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ]", 0-10) = 10 S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ]", 0-11) = 0 S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ]", 0-12) = s S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ]", 0-13) = t S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ]", 0-14) = v S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ]", 0-15) = x S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ]", 0-0) = 100 S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ]", 0-1) = 10 S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ]", 0-2) = d + 10 S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ]", 0-3) = ? S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ]", 0-4) = 200 S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ]", 0-5) = 10 S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ]", 0-6) = j + 10 S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ]", 0-7) = ? S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ]", 0-8) = 50 S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ]", 0-9) = 10 S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ]", 0-10) = 0 S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ]", 0-11) = r S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ]", 0-12) = s S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ]", 0-13) = t S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ]", 0-14) = v S("f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ]", 0-15) = x S("f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x)", 0-0) = 100 S("f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x)", 0-1) = 10 S("f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x)", 0-2) = d + 10 S("f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x)", 0-3) = ? S("f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x)", 0-4) = 200 S("f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x)", 0-5) = 10 S("f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x)", 0-6) = j + 10 S("f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x)", 0-7) = ? S("f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x)", 0-8) = 50 S("f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x)", 0-9) = 10 S("f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x)", 0-10) = p + 10 S("f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x)", 0-11) = ? S("f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x)", 0-12) = 20 S("f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x)", 0-13) = 10 S("f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x)", 0-14) = 10 S("f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x)", 0-15) = x S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ]", 0-0) = 100 S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ]", 0-1) = 10 S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ]", 0-2) = d + 10 S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ]", 0-3) = ? S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ]", 0-4) = 200 S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ]", 0-5) = 10 S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ]", 0-6) = j + 10 S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ]", 0-7) = ? S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ]", 0-8) = 50 S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ]", 0-9) = 10 S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ]", 0-10) = 10 S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ]", 0-11) = ? S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ]", 0-12) = s S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ]", 0-13) = t S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ]", 0-14) = v S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ]", 0-15) = x S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ]", 0-0) = 100 S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ]", 0-1) = 10 S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ]", 0-2) = d + 10 S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ]", 0-3) = ? S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ]", 0-4) = 200 S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ]", 0-5) = 10 S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ]", 0-6) = j + 10 S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ]", 0-7) = ? S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ]", 0-8) = 50 S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ]", 0-9) = 10 S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ]", 0-10) = 10 S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ]", 0-11) = ? S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ]", 0-12) = s S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ]", 0-13) = t S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ]", 0-14) = v S("f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ]", 0-15) = x S("f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ]", 0-0) = 100 S("f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ]", 0-1) = 10 S("f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ]", 0-2) = d + 10 S("f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ]", 0-3) = ? S("f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ]", 0-4) = 200 S("f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ]", 0-5) = 10 S("f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ]", 0-6) = j + 10 S("f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ]", 0-7) = ? S("f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ]", 0-8) = 50 S("f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ]", 0-9) = 10 S("f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ]", 0-10) = p + 10 S("f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ]", 0-11) = ? S("f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ]", 0-12) = 20 S("f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ]", 0-13) = 10 S("f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ]", 0-14) = 10 S("f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ]", 0-15) = 0 S("f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ]", 0-0) = 100 S("f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ]", 0-1) = 10 S("f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ]", 0-2) = d + 10 S("f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ]", 0-3) = ? S("f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ]", 0-4) = 200 S("f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ]", 0-5) = 10 S("f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ]", 0-6) = j + 10 S("f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ]", 0-7) = ? S("f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ]", 0-8) = 50 S("f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ]", 0-9) = 10 S("f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ]", 0-10) = p + 10 S("f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ]", 0-11) = ? S("f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ]", 0-12) = 20 S("f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ]", 0-13) = 10 S("f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ]", 0-14) = 10 S("f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ]", 0-15) = 20 orients the transitions f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ] f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ] f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ] weakly and the transitions f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ] f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ] f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ] strictly and produces the following problem: 8: T: (20, 1) f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x + 1) [ s >= x + 1 ] (15, 1) f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f149(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, 0) [ v >= 1 ] (3850, 1) f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, r + 1, s, t, v, x) [ m >= r + 1 ] (15, 1) f109(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ r >= m ] (15, 1) f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f146(a, b, d, f, g, h, j, l, m, n, p, r, s, t, 10, x) (15, 1) f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) [ p = 0 ] (15, 1) f106(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f109(a, b, d, f, g, h, j, l, m, n, p, 0, s, t, v, x) [ p >= 1 ] (15, 1) f137(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f140(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ t >= 1 ] (3850, 1) f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, l + 1, m, n, p, r, s, t, v, x) [ g >= l + 1 ] (15, 1) f69(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ l >= g ] (15, 1) f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 0, r, s, t, v, x) (15, 1) f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f106(a, b, d, f, g, h, j, l, m, n, 10, r, s, t, v, x) (15, 1) f125(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f137(a, b, d, f, g, h, j, l, m, n, p, r, 20, 10, v, x) (15, 1) f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) [ j = 0 ] (15, 1) f66(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f69(a, b, d, f, g, h, j, 0, m, n, p, r, s, t, v, x) [ j >= 1 ] (15, 1) f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f125(a, b, d, f, g, h, j, l, m, 0, p, r, s, t, v, x) [ n = 0 ] (15, 1) f97(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f100(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ n >= 1 ] (3850, 1) f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, f + 1, g, h, j, l, m, n, p, r, s, t, v, x) [ a >= f + 1 ] (15, 1) f29(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ f >= a ] (15, 1) f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 0, l, m, n, p, r, s, t, v, x) (15, 1) f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f66(a, b, d, f, g, h, 10, l, m, n, p, r, s, t, v, x) (15, 1) f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 0, p, r, s, t, v, x) (15, 1) f85(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f97(a, b, d, f, g, h, j, l, 50, 10, p, r, s, t, v, x) (1, 1) f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) [ d = 0 ] (1, 1) f26(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f29(a, b, d, 0, g, h, j, l, m, n, p, r, s, t, v, x) [ d >= 1 ] (15, 1) f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f85(a, b, d, f, g, 0, j, l, m, n, p, r, s, t, v, x) [ h = 0 ] (15, 1) f57(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f60(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ h >= 1 ] (1, 1) f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 0, f, g, h, j, l, m, n, p, r, s, t, v, x) (1, 1) f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f26(a, b, 10, f, g, h, j, l, m, n, p, r, s, t, v, x) (15, 1) f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 0, j, l, m, n, p, r, s, t, v, x) (15, 1) f45(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f57(a, b, d, f, 200, 10, j, l, m, n, p, r, s, t, v, x) (1, 1) f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f45(a, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b = 0 ] (1, 1) f17(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f20(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) [ b >= 1 ] (1, 1) f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 0, d, f, g, h, j, l, m, n, p, r, s, t, v, x) (1, 1) f0(a, b, d, f, g, h, j, l, m, n, p, r, s, t, v, x) -> f17(100, 10, d, f, g, h, j, l, m, n, p, r, s, t, v, x) start location: f0 leaf cost: 5 Complexity upper bound 11928 Time: 4.232 sec (SMT: 2.267 sec)