YES(?, 129) 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) -> f2(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ a >= b + 1 ] (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) -> f2(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ b >= a + 1 ] (?, 1) f2(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f3(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ c >= b + 1 ] (?, 1) f2(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f3(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ b >= c + 1 ] (?, 1) f3(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ d >= b + 1 ] (?, 1) f3(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ b >= d + 1 ] (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f5(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ e >= b + 1 ] (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f5(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ b >= e + 1 ] (?, 1) f5(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f6(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ f >= b + 1 ] (?, 1) f5(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f6(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ b >= f + 1 ] (?, 1) f6(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ g >= b + 1 ] (?, 1) f6(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ b >= g + 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) -> f18(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ 0 >= h + 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) -> f18(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ h >= 1 ] (?, 1) f18(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f19(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ c >= a + 1 ] (?, 1) f18(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f19(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ a >= c + 1 ] (?, 1) f19(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f20(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ d >= a + 1 ] (?, 1) f19(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f20(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ a >= d + 1 ] (?, 1) f20(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ e >= a + 1 ] (?, 1) f20(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ a >= e + 1 ] (?, 1) f21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f22(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ f >= a + 1 ] (?, 1) f21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f22(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ a >= f + 1 ] (?, 1) f22(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f23(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ g >= a + 1 ] (?, 1) f22(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f23(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ a >= g + 1 ] (?, 1) f33(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f34(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ 0 >= h + 1 ] (?, 1) f33(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f34(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ h >= 1 ] (?, 1) f34(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f35(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ d >= c + 1 ] (?, 1) f34(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f35(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ c >= d + 1 ] (?, 1) f35(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f36(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ e >= c + 1 ] (?, 1) f35(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f36(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ c >= e + 1 ] (?, 1) f36(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f37(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ f >= c + 1 ] (?, 1) f36(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f37(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ c >= f + 1 ] (?, 1) f37(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f38(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ g >= c + 1 ] (?, 1) f37(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f38(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ c >= g + 1 ] (?, 1) f47(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f48(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ 0 >= h + 1 ] (?, 1) f47(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f48(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ h >= 1 ] (?, 1) f48(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f49(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ e >= d + 1 ] (?, 1) f48(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f49(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ d >= e + 1 ] (?, 1) f49(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f50(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ f >= d + 1 ] (?, 1) f49(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f50(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ d >= f + 1 ] (?, 1) f50(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f51(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ g >= d + 1 ] (?, 1) f50(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f51(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ d >= g + 1 ] (?, 1) f59(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f60(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ 0 >= h + 1 ] (?, 1) f59(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f60(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ h >= 1 ] (?, 1) f60(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f61(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ f >= e + 1 ] (?, 1) f60(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f61(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ e >= f + 1 ] (?, 1) f61(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f62(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ g >= e + 1 ] (?, 1) f61(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f62(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ e >= g + 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) -> f70(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ 0 >= h + 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) -> f70(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ h >= 1 ] (?, 1) f70(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ g >= f + 1 ] (?, 1) f70(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ f >= g + 1 ] (?, 1) f77(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f78(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ 0 >= h + 1 ] (?, 1) f77(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f78(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ h >= 1 ] (?, 1) f101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f102(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ 0 >= e + 1 ] (?, 1) f101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f102(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ e >= 1 ] (?, 1) f108(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f109(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ 0 >= h + 1 ] (?, 1) f108(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f109(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ h >= 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) -> f110(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ 0 >= i + 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) -> f110(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ i >= 1 ] (?, 1) f110(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f111(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ 0 >= j + 1 ] (?, 1) f110(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f111(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) [ j >= 1 ] (?, 1) f7(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f17(a, b, c, d, e, f, g, 1, i, j, k, 1, m, n, o, p, q, r, s, t, u, v) [ k >= b + 1 ] (?, 1) f7(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f17(a, b, c, d, e, f, g, 1, i, j, k, 1, m, n, o, p, q, r, s, t, u, v) [ b >= k + 1 ] (?, 1) f7(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f17(a, b, c, d, e, f, g, 0, i, j, b, 0, m, n, o, p, q, r, s, t, u, v) [ b = k ] (?, 1) f6(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f17(a, b, c, d, e, f, b, 0, i, j, k, 0, m, n, o, p, q, r, s, t, u, v) [ b = g ] (?, 1) f5(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f17(a, b, c, d, e, b, g, 0, i, j, k, 0, m, n, o, p, q, r, s, t, u, v) [ b = f ] (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f17(a, b, c, d, b, f, g, 0, i, j, k, 0, m, n, o, p, q, r, s, t, u, v) [ b = e ] (?, 1) f3(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f17(a, b, c, b, e, f, g, 0, i, j, k, 0, m, n, o, p, q, r, s, t, u, v) [ b = d ] (?, 1) f2(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f17(a, b, b, d, e, f, g, 0, i, j, k, 0, m, n, o, p, q, r, s, t, u, v) [ b = c ] (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) -> f17(b, b, c, d, e, f, g, 0, i, j, k, 0, m, n, o, p, q, r, s, t, u, v) [ b = a ] (?, 1) f23(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f33(a, b, c, d, e, f, g, 1, i, j, k, l, 1, n, o, p, q, r, s, t, u, v) [ k >= a + 1 ] (?, 1) f23(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f33(a, b, c, d, e, f, g, 1, i, j, k, l, 1, n, o, p, q, r, s, t, u, v) [ a >= k + 1 ] (?, 1) f23(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f33(a, b, c, d, e, f, g, 0, i, j, a, l, 0, n, o, p, q, r, s, t, u, v) [ a = k ] (?, 1) f22(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f33(a, b, c, d, e, f, a, 0, i, j, k, l, 0, n, o, p, q, r, s, t, u, v) [ a = g ] (?, 1) f21(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f33(a, b, c, d, e, a, g, 0, i, j, k, l, 0, n, o, p, q, r, s, t, u, v) [ a = f ] (?, 1) f20(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f33(a, b, c, d, a, f, g, 0, i, j, k, l, 0, n, o, p, q, r, s, t, u, v) [ a = e ] (?, 1) f19(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f33(a, b, c, a, e, f, g, 0, i, j, k, l, 0, n, o, p, q, r, s, t, u, v) [ a = d ] (?, 1) f18(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f33(a, b, a, d, e, f, g, 0, i, j, k, l, 0, n, o, p, q, r, s, t, u, v) [ a = c ] (?, 1) f17(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f33(a, b, c, d, e, f, g, 0, i, j, k, l, 0, n, o, p, q, r, s, t, u, v) [ h = 0 ] (?, 1) f38(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f47(a, b, c, d, e, f, g, 1, i, j, k, l, m, 1, o, p, q, r, s, t, u, v) [ k >= c + 1 ] (?, 1) f38(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f47(a, b, c, d, e, f, g, 1, i, j, k, l, m, 1, o, p, q, r, s, t, u, v) [ c >= k + 1 ] (?, 1) f38(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f47(a, b, c, d, e, f, g, 0, i, j, c, l, m, 0, o, p, q, r, s, t, u, v) [ c = k ] (?, 1) f37(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f47(a, b, c, d, e, f, c, 0, i, j, k, l, m, 0, o, p, q, r, s, t, u, v) [ c = g ] (?, 1) f36(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f47(a, b, c, d, e, c, g, 0, i, j, k, l, m, 0, o, p, q, r, s, t, u, v) [ c = f ] (?, 1) f35(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f47(a, b, c, d, c, f, g, 0, i, j, k, l, m, 0, o, p, q, r, s, t, u, v) [ c = e ] (?, 1) f34(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f47(a, b, c, c, e, f, g, 0, i, j, k, l, m, 0, o, p, q, r, s, t, u, v) [ c = d ] (?, 1) f33(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f47(a, b, c, d, e, f, g, 0, i, j, k, l, m, 0, o, p, q, r, s, t, u, v) [ h = 0 ] (?, 1) f51(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f59(a, b, c, d, e, f, g, 1, i, j, k, l, m, n, 1, p, q, r, s, t, u, v) [ k >= d + 1 ] (?, 1) f51(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f59(a, b, c, d, e, f, g, 1, i, j, k, l, m, n, 1, p, q, r, s, t, u, v) [ d >= k + 1 ] (?, 1) f51(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f59(a, b, c, d, e, f, g, 0, i, j, d, l, m, n, 0, p, q, r, s, t, u, v) [ d = k ] (?, 1) f50(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f59(a, b, c, d, e, f, d, 0, i, j, k, l, m, n, 0, p, q, r, s, t, u, v) [ d = g ] (?, 1) f49(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f59(a, b, c, d, e, d, g, 0, i, j, k, l, m, n, 0, p, q, r, s, t, u, v) [ d = f ] (?, 1) f48(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f59(a, b, c, d, d, f, g, 0, i, j, k, l, m, n, 0, p, q, r, s, t, u, v) [ d = e ] (?, 1) f47(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f59(a, b, c, d, e, f, g, 0, i, j, k, l, m, n, 0, p, q, r, s, t, u, v) [ h = 0 ] (?, 1) f62(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f69(a, b, c, d, e, f, g, 1, i, j, k, l, m, n, o, 1, q, r, s, t, u, v) [ k >= e + 1 ] (?, 1) f62(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f69(a, b, c, d, e, f, g, 1, i, j, k, l, m, n, o, 1, q, r, s, t, u, v) [ e >= k + 1 ] (?, 1) f62(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f69(a, b, c, d, e, f, g, 0, i, j, e, l, m, n, o, 0, q, r, s, t, u, v) [ e = k ] (?, 1) f61(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f69(a, b, c, d, e, f, e, 0, i, j, k, l, m, n, o, 0, q, r, s, t, u, v) [ e = g ] (?, 1) f60(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f69(a, b, c, d, e, e, g, 0, i, j, k, l, m, n, o, 0, q, r, s, t, u, v) [ e = f ] (?, 1) f59(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f69(a, b, c, d, e, f, g, 0, i, j, k, l, m, n, o, 0, q, r, s, t, u, v) [ h = 0 ] (?, 1) f71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f77(a, b, c, d, e, f, g, 1, i, j, k, l, m, n, o, p, 1, r, s, t, u, v) [ k >= f + 1 ] (?, 1) f71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f77(a, b, c, d, e, f, g, 1, i, j, k, l, m, n, o, p, 1, r, s, t, u, v) [ f >= k + 1 ] (?, 1) f71(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f77(a, b, c, d, e, f, g, 0, i, j, f, l, m, n, o, p, 0, r, s, t, u, v) [ f = k ] (?, 1) f70(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f77(a, b, c, d, e, f, f, 0, i, j, k, l, m, n, o, p, 0, r, s, t, u, v) [ f = g ] (?, 1) f69(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f77(a, b, c, d, e, f, g, 0, i, j, k, l, m, n, o, p, 0, r, s, t, u, v) [ h = 0 ] (?, 1) f78(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f83(a, b, c, d, e, f, g, 1, i, j, k, l, m, n, o, p, q, 1, s, t, u, v) [ k >= g + 1 ] (?, 1) f78(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f83(a, b, c, d, e, f, g, 1, i, j, k, l, m, n, o, p, q, 1, s, t, u, v) [ g >= k + 1 ] (?, 1) f78(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f83(a, b, c, d, e, f, g, 0, i, j, g, l, m, n, o, p, q, 0, s, t, u, v) [ g = k ] (?, 1) f77(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f83(a, b, c, d, e, f, g, 0, i, j, k, l, m, n, o, p, q, 0, s, t, u, v) [ h = 0 ] (?, 1) f83(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f101(a, b, c, d, e, f, g, h, 1, j, k, l, m, n, o, p, q, r, 1, t, u, v) [ 9 >= k /\ 9 >= g /\ 9 >= f /\ 9 >= e /\ 9 >= d /\ 9 >= c /\ 9 >= b /\ 9 >= a ] (?, 1) f83(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f101(a, b, c, d, e, f, g, h, 0, j, k, l, m, n, o, p, q, r, 0, t, u, v) [ k >= 10 /\ 9 >= g /\ 9 >= f /\ 9 >= e /\ 9 >= d /\ 9 >= c /\ 9 >= b /\ 9 >= a ] (?, 1) f83(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f101(a, b, c, d, e, f, g, h, 0, j, k, l, m, n, o, p, q, r, 0, t, u, v) [ g >= 10 /\ 9 >= f /\ 9 >= e /\ 9 >= d /\ 9 >= c /\ 9 >= b /\ 9 >= a ] (?, 1) f83(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f101(a, b, c, d, e, f, g, h, 0, j, k, l, m, n, o, p, q, r, 0, t, u, v) [ f >= 10 /\ 9 >= e /\ 9 >= d /\ 9 >= c /\ 9 >= b /\ 9 >= a ] (?, 1) f83(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f101(a, b, c, d, e, f, g, h, 0, j, k, l, m, n, o, p, q, r, 0, t, u, v) [ e >= 10 /\ 9 >= d /\ 9 >= c /\ 9 >= b /\ 9 >= a ] (?, 1) f83(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f101(a, b, c, d, e, f, g, h, 0, j, k, l, m, n, o, p, q, r, 0, t, u, v) [ d >= 10 /\ 9 >= c /\ 9 >= b /\ 9 >= a ] (?, 1) f83(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f101(a, b, c, d, e, f, g, h, 0, j, k, l, m, n, o, p, q, r, 0, t, u, v) [ c >= 10 /\ 9 >= b /\ 9 >= a ] (?, 1) f83(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f101(a, b, c, d, e, f, g, h, 0, j, k, l, m, n, o, p, q, r, 0, t, u, v) [ 9 >= b /\ a >= 10 ] (?, 1) f83(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f101(a, b, c, d, e, f, g, h, 0, j, k, l, m, n, o, p, q, r, 0, t, u, v) [ b >= 10 ] (?, 1) f102(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f108(a, b, c, d, e, f, g, h, i, 1, k, l, m, n, o, p, q, r, s, 1, w, v) [ 0 >= b + 1 ] (?, 1) f102(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f108(a, b, c, d, e, f, g, h, i, 1, k, l, m, n, o, p, q, r, s, 1, w, v) [ b >= 1 ] (?, 1) f102(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f108(a, 0, c, d, e, f, g, h, i, 0, k, l, m, n, o, p, q, r, s, 0, w, v) [ b = 0 ] (?, 1) f101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f108(a, b, c, d, 0, f, g, h, i, 0, k, l, m, n, o, p, q, r, s, 0, w, v) [ e = 0 ] (?, 1) f111(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f119(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, 0) [ 0 >= u + 1 ] (?, 1) f111(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f119(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, 0) [ u >= 1 ] (?, 1) f111(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f119(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, 0, 1) [ u = 0 ] (?, 1) f110(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f119(a, b, c, d, e, f, g, h, i, 0, k, l, m, n, o, p, q, r, s, t, u, 1) [ j = 0 ] (?, 1) f109(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f119(a, b, c, d, e, f, g, h, 0, j, k, l, m, n, o, p, q, r, s, t, u, 1) [ i = 0 ] (?, 1) f108(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -> f119(a, b, c, d, e, f, g, 0, i, j, k, l, m, n, o, p, q, r, s, t, u, 1) [ h = 0 ] start location: f0 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c, d, e, f, g, h, i, j, k, u]. We thus obtain the following problem: 2: T: (?, 1) f108(a, b, c, d, e, f, g, h, i, j, k, u) -> f119(a, b, c, d, e, f, g, 0, i, j, k, u) [ h = 0 ] (?, 1) f109(a, b, c, d, e, f, g, h, i, j, k, u) -> f119(a, b, c, d, e, f, g, h, 0, j, k, u) [ i = 0 ] (?, 1) f110(a, b, c, d, e, f, g, h, i, j, k, u) -> f119(a, b, c, d, e, f, g, h, i, 0, k, u) [ j = 0 ] (?, 1) f111(a, b, c, d, e, f, g, h, i, j, k, u) -> f119(a, b, c, d, e, f, g, h, i, j, k, 0) [ u = 0 ] (?, 1) f111(a, b, c, d, e, f, g, h, i, j, k, u) -> f119(a, b, c, d, e, f, g, h, i, j, k, u) [ u >= 1 ] (?, 1) f111(a, b, c, d, e, f, g, h, i, j, k, u) -> f119(a, b, c, d, e, f, g, h, i, j, k, u) [ 0 >= u + 1 ] (?, 1) f101(a, b, c, d, e, f, g, h, i, j, k, u) -> f108(a, b, c, d, 0, f, g, h, i, 0, k, w) [ e = 0 ] (?, 1) f102(a, b, c, d, e, f, g, h, i, j, k, u) -> f108(a, 0, c, d, e, f, g, h, i, 0, k, w) [ b = 0 ] (?, 1) f102(a, b, c, d, e, f, g, h, i, j, k, u) -> f108(a, b, c, d, e, f, g, h, i, 1, k, w) [ b >= 1 ] (?, 1) f102(a, b, c, d, e, f, g, h, i, j, k, u) -> f108(a, b, c, d, e, f, g, h, i, 1, k, w) [ 0 >= b + 1 ] (?, 1) f83(a, b, c, d, e, f, g, h, i, j, k, u) -> f101(a, b, c, d, e, f, g, h, 0, j, k, u) [ b >= 10 ] (?, 1) f83(a, b, c, d, e, f, g, h, i, j, k, u) -> f101(a, b, c, d, e, f, g, h, 0, j, k, u) [ 9 >= b /\ a >= 10 ] (?, 1) f83(a, b, c, d, e, f, g, h, i, j, k, u) -> f101(a, b, c, d, e, f, g, h, 0, j, k, u) [ c >= 10 /\ 9 >= b /\ 9 >= a ] (?, 1) f83(a, b, c, d, e, f, g, h, i, j, k, u) -> f101(a, b, c, d, e, f, g, h, 0, j, k, u) [ d >= 10 /\ 9 >= c /\ 9 >= b /\ 9 >= a ] (?, 1) f83(a, b, c, d, e, f, g, h, i, j, k, u) -> f101(a, b, c, d, e, f, g, h, 0, j, k, u) [ e >= 10 /\ 9 >= d /\ 9 >= c /\ 9 >= b /\ 9 >= a ] (?, 1) f83(a, b, c, d, e, f, g, h, i, j, k, u) -> f101(a, b, c, d, e, f, g, h, 0, j, k, u) [ f >= 10 /\ 9 >= e /\ 9 >= d /\ 9 >= c /\ 9 >= b /\ 9 >= a ] (?, 1) f83(a, b, c, d, e, f, g, h, i, j, k, u) -> f101(a, b, c, d, e, f, g, h, 0, j, k, u) [ g >= 10 /\ 9 >= f /\ 9 >= e /\ 9 >= d /\ 9 >= c /\ 9 >= b /\ 9 >= a ] (?, 1) f83(a, b, c, d, e, f, g, h, i, j, k, u) -> f101(a, b, c, d, e, f, g, h, 0, j, k, u) [ k >= 10 /\ 9 >= g /\ 9 >= f /\ 9 >= e /\ 9 >= d /\ 9 >= c /\ 9 >= b /\ 9 >= a ] (?, 1) f83(a, b, c, d, e, f, g, h, i, j, k, u) -> f101(a, b, c, d, e, f, g, h, 1, j, k, u) [ 9 >= k /\ 9 >= g /\ 9 >= f /\ 9 >= e /\ 9 >= d /\ 9 >= c /\ 9 >= b /\ 9 >= a ] (?, 1) f77(a, b, c, d, e, f, g, h, i, j, k, u) -> f83(a, b, c, d, e, f, g, 0, i, j, k, u) [ h = 0 ] (?, 1) f78(a, b, c, d, e, f, g, h, i, j, k, u) -> f83(a, b, c, d, e, f, g, 0, i, j, g, u) [ g = k ] (?, 1) f78(a, b, c, d, e, f, g, h, i, j, k, u) -> f83(a, b, c, d, e, f, g, 1, i, j, k, u) [ g >= k + 1 ] (?, 1) f78(a, b, c, d, e, f, g, h, i, j, k, u) -> f83(a, b, c, d, e, f, g, 1, i, j, k, u) [ k >= g + 1 ] (?, 1) f69(a, b, c, d, e, f, g, h, i, j, k, u) -> f77(a, b, c, d, e, f, g, 0, i, j, k, u) [ h = 0 ] (?, 1) f70(a, b, c, d, e, f, g, h, i, j, k, u) -> f77(a, b, c, d, e, f, f, 0, i, j, k, u) [ f = g ] (?, 1) f71(a, b, c, d, e, f, g, h, i, j, k, u) -> f77(a, b, c, d, e, f, g, 0, i, j, f, u) [ f = k ] (?, 1) f71(a, b, c, d, e, f, g, h, i, j, k, u) -> f77(a, b, c, d, e, f, g, 1, i, j, k, u) [ f >= k + 1 ] (?, 1) f71(a, b, c, d, e, f, g, h, i, j, k, u) -> f77(a, b, c, d, e, f, g, 1, i, j, k, u) [ k >= f + 1 ] (?, 1) f59(a, b, c, d, e, f, g, h, i, j, k, u) -> f69(a, b, c, d, e, f, g, 0, i, j, k, u) [ h = 0 ] (?, 1) f60(a, b, c, d, e, f, g, h, i, j, k, u) -> f69(a, b, c, d, e, e, g, 0, i, j, k, u) [ e = f ] (?, 1) f61(a, b, c, d, e, f, g, h, i, j, k, u) -> f69(a, b, c, d, e, f, e, 0, i, j, k, u) [ e = g ] (?, 1) f62(a, b, c, d, e, f, g, h, i, j, k, u) -> f69(a, b, c, d, e, f, g, 0, i, j, e, u) [ e = k ] (?, 1) f62(a, b, c, d, e, f, g, h, i, j, k, u) -> f69(a, b, c, d, e, f, g, 1, i, j, k, u) [ e >= k + 1 ] (?, 1) f62(a, b, c, d, e, f, g, h, i, j, k, u) -> f69(a, b, c, d, e, f, g, 1, i, j, k, u) [ k >= e + 1 ] (?, 1) f47(a, b, c, d, e, f, g, h, i, j, k, u) -> f59(a, b, c, d, e, f, g, 0, i, j, k, u) [ h = 0 ] (?, 1) f48(a, b, c, d, e, f, g, h, i, j, k, u) -> f59(a, b, c, d, d, f, g, 0, i, j, k, u) [ d = e ] (?, 1) f49(a, b, c, d, e, f, g, h, i, j, k, u) -> f59(a, b, c, d, e, d, g, 0, i, j, k, u) [ d = f ] (?, 1) f50(a, b, c, d, e, f, g, h, i, j, k, u) -> f59(a, b, c, d, e, f, d, 0, i, j, k, u) [ d = g ] (?, 1) f51(a, b, c, d, e, f, g, h, i, j, k, u) -> f59(a, b, c, d, e, f, g, 0, i, j, d, u) [ d = k ] (?, 1) f51(a, b, c, d, e, f, g, h, i, j, k, u) -> f59(a, b, c, d, e, f, g, 1, i, j, k, u) [ d >= k + 1 ] (?, 1) f51(a, b, c, d, e, f, g, h, i, j, k, u) -> f59(a, b, c, d, e, f, g, 1, i, j, k, u) [ k >= d + 1 ] (?, 1) f33(a, b, c, d, e, f, g, h, i, j, k, u) -> f47(a, b, c, d, e, f, g, 0, i, j, k, u) [ h = 0 ] (?, 1) f34(a, b, c, d, e, f, g, h, i, j, k, u) -> f47(a, b, c, c, e, f, g, 0, i, j, k, u) [ c = d ] (?, 1) f35(a, b, c, d, e, f, g, h, i, j, k, u) -> f47(a, b, c, d, c, f, g, 0, i, j, k, u) [ c = e ] (?, 1) f36(a, b, c, d, e, f, g, h, i, j, k, u) -> f47(a, b, c, d, e, c, g, 0, i, j, k, u) [ c = f ] (?, 1) f37(a, b, c, d, e, f, g, h, i, j, k, u) -> f47(a, b, c, d, e, f, c, 0, i, j, k, u) [ c = g ] (?, 1) f38(a, b, c, d, e, f, g, h, i, j, k, u) -> f47(a, b, c, d, e, f, g, 0, i, j, c, u) [ c = k ] (?, 1) f38(a, b, c, d, e, f, g, h, i, j, k, u) -> f47(a, b, c, d, e, f, g, 1, i, j, k, u) [ c >= k + 1 ] (?, 1) f38(a, b, c, d, e, f, g, h, i, j, k, u) -> f47(a, b, c, d, e, f, g, 1, i, j, k, u) [ k >= c + 1 ] (?, 1) f17(a, b, c, d, e, f, g, h, i, j, k, u) -> f33(a, b, c, d, e, f, g, 0, i, j, k, u) [ h = 0 ] (?, 1) f18(a, b, c, d, e, f, g, h, i, j, k, u) -> f33(a, b, a, d, e, f, g, 0, i, j, k, u) [ a = c ] (?, 1) f19(a, b, c, d, e, f, g, h, i, j, k, u) -> f33(a, b, c, a, e, f, g, 0, i, j, k, u) [ a = d ] (?, 1) f20(a, b, c, d, e, f, g, h, i, j, k, u) -> f33(a, b, c, d, a, f, g, 0, i, j, k, u) [ a = e ] (?, 1) f21(a, b, c, d, e, f, g, h, i, j, k, u) -> f33(a, b, c, d, e, a, g, 0, i, j, k, u) [ a = f ] (?, 1) f22(a, b, c, d, e, f, g, h, i, j, k, u) -> f33(a, b, c, d, e, f, a, 0, i, j, k, u) [ a = g ] (?, 1) f23(a, b, c, d, e, f, g, h, i, j, k, u) -> f33(a, b, c, d, e, f, g, 0, i, j, a, u) [ a = k ] (?, 1) f23(a, b, c, d, e, f, g, h, i, j, k, u) -> f33(a, b, c, d, e, f, g, 1, i, j, k, u) [ a >= k + 1 ] (?, 1) f23(a, b, c, d, e, f, g, h, i, j, k, u) -> f33(a, b, c, d, e, f, g, 1, i, j, k, u) [ k >= a + 1 ] (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, u) -> f17(b, b, c, d, e, f, g, 0, i, j, k, u) [ b = a ] (?, 1) f2(a, b, c, d, e, f, g, h, i, j, k, u) -> f17(a, b, b, d, e, f, g, 0, i, j, k, u) [ b = c ] (?, 1) f3(a, b, c, d, e, f, g, h, i, j, k, u) -> f17(a, b, c, b, e, f, g, 0, i, j, k, u) [ b = d ] (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, u) -> f17(a, b, c, d, b, f, g, 0, i, j, k, u) [ b = e ] (?, 1) f5(a, b, c, d, e, f, g, h, i, j, k, u) -> f17(a, b, c, d, e, b, g, 0, i, j, k, u) [ b = f ] (?, 1) f6(a, b, c, d, e, f, g, h, i, j, k, u) -> f17(a, b, c, d, e, f, b, 0, i, j, k, u) [ b = g ] (?, 1) f7(a, b, c, d, e, f, g, h, i, j, k, u) -> f17(a, b, c, d, e, f, g, 0, i, j, b, u) [ b = k ] (?, 1) f7(a, b, c, d, e, f, g, h, i, j, k, u) -> f17(a, b, c, d, e, f, g, 1, i, j, k, u) [ b >= k + 1 ] (?, 1) f7(a, b, c, d, e, f, g, h, i, j, k, u) -> f17(a, b, c, d, e, f, g, 1, i, j, k, u) [ k >= b + 1 ] (?, 1) f110(a, b, c, d, e, f, g, h, i, j, k, u) -> f111(a, b, c, d, e, f, g, h, i, j, k, u) [ j >= 1 ] (?, 1) f110(a, b, c, d, e, f, g, h, i, j, k, u) -> f111(a, b, c, d, e, f, g, h, i, j, k, u) [ 0 >= j + 1 ] (?, 1) f109(a, b, c, d, e, f, g, h, i, j, k, u) -> f110(a, b, c, d, e, f, g, h, i, j, k, u) [ i >= 1 ] (?, 1) f109(a, b, c, d, e, f, g, h, i, j, k, u) -> f110(a, b, c, d, e, f, g, h, i, j, k, u) [ 0 >= i + 1 ] (?, 1) f108(a, b, c, d, e, f, g, h, i, j, k, u) -> f109(a, b, c, d, e, f, g, h, i, j, k, u) [ h >= 1 ] (?, 1) f108(a, b, c, d, e, f, g, h, i, j, k, u) -> f109(a, b, c, d, e, f, g, h, i, j, k, u) [ 0 >= h + 1 ] (?, 1) f101(a, b, c, d, e, f, g, h, i, j, k, u) -> f102(a, b, c, d, e, f, g, h, i, j, k, u) [ e >= 1 ] (?, 1) f101(a, b, c, d, e, f, g, h, i, j, k, u) -> f102(a, b, c, d, e, f, g, h, i, j, k, u) [ 0 >= e + 1 ] (?, 1) f77(a, b, c, d, e, f, g, h, i, j, k, u) -> f78(a, b, c, d, e, f, g, h, i, j, k, u) [ h >= 1 ] (?, 1) f77(a, b, c, d, e, f, g, h, i, j, k, u) -> f78(a, b, c, d, e, f, g, h, i, j, k, u) [ 0 >= h + 1 ] (?, 1) f70(a, b, c, d, e, f, g, h, i, j, k, u) -> f71(a, b, c, d, e, f, g, h, i, j, k, u) [ f >= g + 1 ] (?, 1) f70(a, b, c, d, e, f, g, h, i, j, k, u) -> f71(a, b, c, d, e, f, g, h, i, j, k, u) [ g >= f + 1 ] (?, 1) f69(a, b, c, d, e, f, g, h, i, j, k, u) -> f70(a, b, c, d, e, f, g, h, i, j, k, u) [ h >= 1 ] (?, 1) f69(a, b, c, d, e, f, g, h, i, j, k, u) -> f70(a, b, c, d, e, f, g, h, i, j, k, u) [ 0 >= h + 1 ] (?, 1) f61(a, b, c, d, e, f, g, h, i, j, k, u) -> f62(a, b, c, d, e, f, g, h, i, j, k, u) [ e >= g + 1 ] (?, 1) f61(a, b, c, d, e, f, g, h, i, j, k, u) -> f62(a, b, c, d, e, f, g, h, i, j, k, u) [ g >= e + 1 ] (?, 1) f60(a, b, c, d, e, f, g, h, i, j, k, u) -> f61(a, b, c, d, e, f, g, h, i, j, k, u) [ e >= f + 1 ] (?, 1) f60(a, b, c, d, e, f, g, h, i, j, k, u) -> f61(a, b, c, d, e, f, g, h, i, j, k, u) [ f >= e + 1 ] (?, 1) f59(a, b, c, d, e, f, g, h, i, j, k, u) -> f60(a, b, c, d, e, f, g, h, i, j, k, u) [ h >= 1 ] (?, 1) f59(a, b, c, d, e, f, g, h, i, j, k, u) -> f60(a, b, c, d, e, f, g, h, i, j, k, u) [ 0 >= h + 1 ] (?, 1) f50(a, b, c, d, e, f, g, h, i, j, k, u) -> f51(a, b, c, d, e, f, g, h, i, j, k, u) [ d >= g + 1 ] (?, 1) f50(a, b, c, d, e, f, g, h, i, j, k, u) -> f51(a, b, c, d, e, f, g, h, i, j, k, u) [ g >= d + 1 ] (?, 1) f49(a, b, c, d, e, f, g, h, i, j, k, u) -> f50(a, b, c, d, e, f, g, h, i, j, k, u) [ d >= f + 1 ] (?, 1) f49(a, b, c, d, e, f, g, h, i, j, k, u) -> f50(a, b, c, d, e, f, g, h, i, j, k, u) [ f >= d + 1 ] (?, 1) f48(a, b, c, d, e, f, g, h, i, j, k, u) -> f49(a, b, c, d, e, f, g, h, i, j, k, u) [ d >= e + 1 ] (?, 1) f48(a, b, c, d, e, f, g, h, i, j, k, u) -> f49(a, b, c, d, e, f, g, h, i, j, k, u) [ e >= d + 1 ] (?, 1) f47(a, b, c, d, e, f, g, h, i, j, k, u) -> f48(a, b, c, d, e, f, g, h, i, j, k, u) [ h >= 1 ] (?, 1) f47(a, b, c, d, e, f, g, h, i, j, k, u) -> f48(a, b, c, d, e, f, g, h, i, j, k, u) [ 0 >= h + 1 ] (?, 1) f37(a, b, c, d, e, f, g, h, i, j, k, u) -> f38(a, b, c, d, e, f, g, h, i, j, k, u) [ c >= g + 1 ] (?, 1) f37(a, b, c, d, e, f, g, h, i, j, k, u) -> f38(a, b, c, d, e, f, g, h, i, j, k, u) [ g >= c + 1 ] (?, 1) f36(a, b, c, d, e, f, g, h, i, j, k, u) -> f37(a, b, c, d, e, f, g, h, i, j, k, u) [ c >= f + 1 ] (?, 1) f36(a, b, c, d, e, f, g, h, i, j, k, u) -> f37(a, b, c, d, e, f, g, h, i, j, k, u) [ f >= c + 1 ] (?, 1) f35(a, b, c, d, e, f, g, h, i, j, k, u) -> f36(a, b, c, d, e, f, g, h, i, j, k, u) [ c >= e + 1 ] (?, 1) f35(a, b, c, d, e, f, g, h, i, j, k, u) -> f36(a, b, c, d, e, f, g, h, i, j, k, u) [ e >= c + 1 ] (?, 1) f34(a, b, c, d, e, f, g, h, i, j, k, u) -> f35(a, b, c, d, e, f, g, h, i, j, k, u) [ c >= d + 1 ] (?, 1) f34(a, b, c, d, e, f, g, h, i, j, k, u) -> f35(a, b, c, d, e, f, g, h, i, j, k, u) [ d >= c + 1 ] (?, 1) f33(a, b, c, d, e, f, g, h, i, j, k, u) -> f34(a, b, c, d, e, f, g, h, i, j, k, u) [ h >= 1 ] (?, 1) f33(a, b, c, d, e, f, g, h, i, j, k, u) -> f34(a, b, c, d, e, f, g, h, i, j, k, u) [ 0 >= h + 1 ] (?, 1) f22(a, b, c, d, e, f, g, h, i, j, k, u) -> f23(a, b, c, d, e, f, g, h, i, j, k, u) [ a >= g + 1 ] (?, 1) f22(a, b, c, d, e, f, g, h, i, j, k, u) -> f23(a, b, c, d, e, f, g, h, i, j, k, u) [ g >= a + 1 ] (?, 1) f21(a, b, c, d, e, f, g, h, i, j, k, u) -> f22(a, b, c, d, e, f, g, h, i, j, k, u) [ a >= f + 1 ] (?, 1) f21(a, b, c, d, e, f, g, h, i, j, k, u) -> f22(a, b, c, d, e, f, g, h, i, j, k, u) [ f >= a + 1 ] (?, 1) f20(a, b, c, d, e, f, g, h, i, j, k, u) -> f21(a, b, c, d, e, f, g, h, i, j, k, u) [ a >= e + 1 ] (?, 1) f20(a, b, c, d, e, f, g, h, i, j, k, u) -> f21(a, b, c, d, e, f, g, h, i, j, k, u) [ e >= a + 1 ] (?, 1) f19(a, b, c, d, e, f, g, h, i, j, k, u) -> f20(a, b, c, d, e, f, g, h, i, j, k, u) [ a >= d + 1 ] (?, 1) f19(a, b, c, d, e, f, g, h, i, j, k, u) -> f20(a, b, c, d, e, f, g, h, i, j, k, u) [ d >= a + 1 ] (?, 1) f18(a, b, c, d, e, f, g, h, i, j, k, u) -> f19(a, b, c, d, e, f, g, h, i, j, k, u) [ a >= c + 1 ] (?, 1) f18(a, b, c, d, e, f, g, h, i, j, k, u) -> f19(a, b, c, d, e, f, g, h, i, j, k, u) [ c >= a + 1 ] (?, 1) f17(a, b, c, d, e, f, g, h, i, j, k, u) -> f18(a, b, c, d, e, f, g, h, i, j, k, u) [ h >= 1 ] (?, 1) f17(a, b, c, d, e, f, g, h, i, j, k, u) -> f18(a, b, c, d, e, f, g, h, i, j, k, u) [ 0 >= h + 1 ] (?, 1) f6(a, b, c, d, e, f, g, h, i, j, k, u) -> f7(a, b, c, d, e, f, g, h, i, j, k, u) [ b >= g + 1 ] (?, 1) f6(a, b, c, d, e, f, g, h, i, j, k, u) -> f7(a, b, c, d, e, f, g, h, i, j, k, u) [ g >= b + 1 ] (?, 1) f5(a, b, c, d, e, f, g, h, i, j, k, u) -> f6(a, b, c, d, e, f, g, h, i, j, k, u) [ b >= f + 1 ] (?, 1) f5(a, b, c, d, e, f, g, h, i, j, k, u) -> f6(a, b, c, d, e, f, g, h, i, j, k, u) [ f >= b + 1 ] (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, u) -> f5(a, b, c, d, e, f, g, h, i, j, k, u) [ b >= e + 1 ] (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, u) -> f5(a, b, c, d, e, f, g, h, i, j, k, u) [ e >= b + 1 ] (?, 1) f3(a, b, c, d, e, f, g, h, i, j, k, u) -> f4(a, b, c, d, e, f, g, h, i, j, k, u) [ b >= d + 1 ] (?, 1) f3(a, b, c, d, e, f, g, h, i, j, k, u) -> f4(a, b, c, d, e, f, g, h, i, j, k, u) [ d >= b + 1 ] (?, 1) f2(a, b, c, d, e, f, g, h, i, j, k, u) -> f3(a, b, c, d, e, f, g, h, i, j, k, u) [ b >= c + 1 ] (?, 1) f2(a, b, c, d, e, f, g, h, i, j, k, u) -> f3(a, b, c, d, e, f, g, h, i, j, k, u) [ c >= b + 1 ] (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, u) -> f2(a, b, c, d, e, f, g, h, i, j, k, u) [ b >= a + 1 ] (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, u) -> f2(a, b, c, d, e, f, g, h, i, j, k, u) [ a >= b + 1 ] start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (none) start location: f0 leaf cost: 129 Complexity upper bound 129 Time: 2.105 sec (SMT: 1.522 sec)