MAYBE Initial complexity problem: 1: T: (?, 1) f1(a, b, c, d, e, f, g, h) -> f1(a, b, i, j, k, f, g, h) [ b >= a + 1 ] (?, 1) f1(a, b, c, d, e, f, g, h) -> f300(a, b, i, j, e, k, g, h) [ a >= b ] (1, 1) f2(a, b, c, d, e, f, g, h) -> f1(a, b, c, d, e, f, i, j) start location: f2 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem: 2: T: (?, 1) f1(a, b, c, d, e, f, g, h) -> f1(a, b, i, j, k, f, g, h) [ b >= a + 1 ] (1, 1) f2(a, b, c, d, e, f, g, h) -> f1(a, b, c, d, e, f, i, j) start location: f2 leaf cost: 1 By chaining the transition f2(a, b, c, d, e, f, g, h) -> f1(a, b, c, d, e, f, i, j) with all transitions in problem 2, the following new transition is obtained: f2(a, b, c, d, e, f, g, h) -> f1(a, b, i', j', k, f, i, j) [ b >= a + 1 ] We thus obtain the following problem: 3: T: (1, 2) f2(a, b, c, d, e, f, g, h) -> f1(a, b, i', j', k, f, i, j) [ b >= a + 1 ] (?, 1) f1(a, b, c, d, e, f, g, h) -> f1(a, b, i, j, k, f, g, h) [ b >= a + 1 ] start location: f2 leaf cost: 1 By chaining the transition f2(a, b, c, d, e, f, g, h) -> f1(a, b, i', j', k, f, i, j) [ b >= a + 1 ] with all transitions in problem 3, the following new transition is obtained: f2(a, b, c, d, e, f, g, h) -> f1(a, b, i'', j'', k', f, i, j) [ b >= a + 1 ] We thus obtain the following problem: 4: T: (1, 3) f2(a, b, c, d, e, f, g, h) -> f1(a, b, i'', j'', k', f, i, j) [ b >= a + 1 ] (?, 1) f1(a, b, c, d, e, f, g, h) -> f1(a, b, i, j, k, f, g, h) [ b >= a + 1 ] start location: f2 leaf cost: 1 By chaining the transition f2(a, b, c, d, e, f, g, h) -> f1(a, b, i'', j'', k', f, i, j) [ b >= a + 1 ] with all transitions in problem 4, the following new transition is obtained: f2(a, b, c, d, e, f, g, h) -> f1(a, b, i', j', k, f, i, j) [ b >= a + 1 ] We thus obtain the following problem: 5: T: (1, 4) f2(a, b, c, d, e, f, g, h) -> f1(a, b, i', j', k, f, i, j) [ b >= a + 1 ] (?, 1) f1(a, b, c, d, e, f, g, h) -> f1(a, b, i, j, k, f, g, h) [ b >= a + 1 ] start location: f2 leaf cost: 1 By chaining the transition f2(a, b, c, d, e, f, g, h) -> f1(a, b, i', j', k, f, i, j) [ b >= a + 1 ] with all transitions in problem 5, the following new transition is obtained: f2(a, b, c, d, e, f, g, h) -> f1(a, b, i'', j'', k', f, i, j) [ b >= a + 1 ] We thus obtain the following problem: 6: T: (1, 5) f2(a, b, c, d, e, f, g, h) -> f1(a, b, i'', j'', k', f, i, j) [ b >= a + 1 ] (?, 1) f1(a, b, c, d, e, f, g, h) -> f1(a, b, i, j, k, f, g, h) [ b >= a + 1 ] start location: f2 leaf cost: 1 By chaining the transition f2(a, b, c, d, e, f, g, h) -> f1(a, b, i'', j'', k', f, i, j) [ b >= a + 1 ] with all transitions in problem 6, the following new transition is obtained: f2(a, b, c, d, e, f, g, h) -> f1(a, b, i', j', k, f, i, j) [ b >= a + 1 ] We thus obtain the following problem: 7: T: (1, 6) f2(a, b, c, d, e, f, g, h) -> f1(a, b, i', j', k, f, i, j) [ b >= a + 1 ] (?, 1) f1(a, b, c, d, e, f, g, h) -> f1(a, b, i, j, k, f, g, h) [ b >= a + 1 ] start location: f2 leaf cost: 1 By chaining the transition f2(a, b, c, d, e, f, g, h) -> f1(a, b, i', j', k, f, i, j) [ b >= a + 1 ] with all transitions in problem 7, the following new transition is obtained: f2(a, b, c, d, e, f, g, h) -> f1(a, b, i'', j'', k', f, i, j) [ b >= a + 1 ] We thus obtain the following problem: 8: T: (1, 7) f2(a, b, c, d, e, f, g, h) -> f1(a, b, i'', j'', k', f, i, j) [ b >= a + 1 ] (?, 1) f1(a, b, c, d, e, f, g, h) -> f1(a, b, i, j, k, f, g, h) [ b >= a + 1 ] start location: f2 leaf cost: 1 By chaining the transition f2(a, b, c, d, e, f, g, h) -> f1(a, b, i'', j'', k', f, i, j) [ b >= a + 1 ] with all transitions in problem 8, the following new transition is obtained: f2(a, b, c, d, e, f, g, h) -> f1(a, b, i', j', k, f, i, j) [ b >= a + 1 ] We thus obtain the following problem: 9: T: (1, 8) f2(a, b, c, d, e, f, g, h) -> f1(a, b, i', j', k, f, i, j) [ b >= a + 1 ] (?, 1) f1(a, b, c, d, e, f, g, h) -> f1(a, b, i, j, k, f, g, h) [ b >= a + 1 ] start location: f2 leaf cost: 1 By chaining the transition f2(a, b, c, d, e, f, g, h) -> f1(a, b, i', j', k, f, i, j) [ b >= a + 1 ] with all transitions in problem 9, the following new transition is obtained: f2(a, b, c, d, e, f, g, h) -> f1(a, b, i'', j'', k', f, i, j) [ b >= a + 1 ] We thus obtain the following problem: 10: T: (1, 9) f2(a, b, c, d, e, f, g, h) -> f1(a, b, i'', j'', k', f, i, j) [ b >= a + 1 ] (?, 1) f1(a, b, c, d, e, f, g, h) -> f1(a, b, i, j, k, f, g, h) [ b >= a + 1 ] start location: f2 leaf cost: 1 By chaining the transition f2(a, b, c, d, e, f, g, h) -> f1(a, b, i'', j'', k', f, i, j) [ b >= a + 1 ] with all transitions in problem 10, the following new transition is obtained: f2(a, b, c, d, e, f, g, h) -> f1(a, b, i', j', k, f, i, j) [ b >= a + 1 ] We thus obtain the following problem: 11: T: (1, 10) f2(a, b, c, d, e, f, g, h) -> f1(a, b, i', j', k, f, i, j) [ b >= a + 1 ] (?, 1) f1(a, b, c, d, e, f, g, h) -> f1(a, b, i, j, k, f, g, h) [ b >= a + 1 ] start location: f2 leaf cost: 1 By chaining the transition f2(a, b, c, d, e, f, g, h) -> f1(a, b, i', j', k, f, i, j) [ b >= a + 1 ] with all transitions in problem 11, the following new transition is obtained: f2(a, b, c, d, e, f, g, h) -> f1(a, b, i'', j'', k', f, i, j) [ b >= a + 1 ] We thus obtain the following problem: 12: T: (1, 11) f2(a, b, c, d, e, f, g, h) -> f1(a, b, i'', j'', k', f, i, j) [ b >= a + 1 ] (?, 1) f1(a, b, c, d, e, f, g, h) -> f1(a, b, i, j, k, f, g, h) [ b >= a + 1 ] start location: f2 leaf cost: 1 By chaining the transition f2(a, b, c, d, e, f, g, h) -> f1(a, b, i'', j'', k', f, i, j) [ b >= a + 1 ] with all transitions in problem 12, the following new transition is obtained: f2(a, b, c, d, e, f, g, h) -> f1(a, b, i', j', k, f, i, j) [ b >= a + 1 ] We thus obtain the following problem: 13: T: (1, 12) f2(a, b, c, d, e, f, g, h) -> f1(a, b, i', j', k, f, i, j) [ b >= a + 1 ] (?, 1) f1(a, b, c, d, e, f, g, h) -> f1(a, b, i, j, k, f, g, h) [ b >= a + 1 ] start location: f2 leaf cost: 1 By chaining the transition f2(a, b, c, d, e, f, g, h) -> f1(a, b, i', j', k, f, i, j) [ b >= a + 1 ] with all transitions in problem 13, the following new transition is obtained: f2(a, b, c, d, e, f, g, h) -> f1(a, b, i'', j'', k', f, i, j) [ b >= a + 1 ] We thus obtain the following problem: 14: T: (1, 13) f2(a, b, c, d, e, f, g, h) -> f1(a, b, i'', j'', k', f, i, j) [ b >= a + 1 ] (?, 1) f1(a, b, c, d, e, f, g, h) -> f1(a, b, i, j, k, f, g, h) [ b >= a + 1 ] start location: f2 leaf cost: 1 By chaining the transition f2(a, b, c, d, e, f, g, h) -> f1(a, b, i'', j'', k', f, i, j) [ b >= a + 1 ] with all transitions in problem 14, the following new transition is obtained: f2(a, b, c, d, e, f, g, h) -> f1(a, b, i', j', k, f, i, j) [ b >= a + 1 ] We thus obtain the following problem: 15: T: (1, 14) f2(a, b, c, d, e, f, g, h) -> f1(a, b, i', j', k, f, i, j) [ b >= a + 1 ] (?, 1) f1(a, b, c, d, e, f, g, h) -> f1(a, b, i, j, k, f, g, h) [ b >= a + 1 ] start location: f2 leaf cost: 1 By chaining the transition f2(a, b, c, d, e, f, g, h) -> f1(a, b, i', j', k, f, i, j) [ b >= a + 1 ] with all transitions in problem 15, the following new transition is obtained: f2(a, b, c, d, e, f, g, h) -> f1(a, b, i'', j'', k', f, i, j) [ b >= a + 1 ] We thus obtain the following problem: 16: T: (1, 15) f2(a, b, c, d, e, f, g, h) -> f1(a, b, i'', j'', k', f, i, j) [ b >= a + 1 ] (?, 1) f1(a, b, c, d, e, f, g, h) -> f1(a, b, i, j, k, f, g, h) [ b >= a + 1 ] start location: f2 leaf cost: 1 By chaining the transition f2(a, b, c, d, e, f, g, h) -> f1(a, b, i'', j'', k', f, i, j) [ b >= a + 1 ] with all transitions in problem 16, the following new transition is obtained: f2(a, b, c, d, e, f, g, h) -> f1(a, b, i', j', k, f, i, j) [ b >= a + 1 ] We thus obtain the following problem: 17: T: (1, 16) f2(a, b, c, d, e, f, g, h) -> f1(a, b, i', j', k, f, i, j) [ b >= a + 1 ] (?, 1) f1(a, b, c, d, e, f, g, h) -> f1(a, b, i, j, k, f, g, h) [ b >= a + 1 ] start location: f2 leaf cost: 1 Complexity upper bound ? Time: 1.231 sec (SMT: 1.145 sec)