MAYBE Initial complexity problem: 1: T: (1, 1) f0(a, b, c, d, e, f, g, h) -> f15(10, 35, 285, i, i, 0, g, h) (?, 1) f15(a, b, c, d, e, f, g, h) -> f25(a, b, c, d, e, f, i, 1) [ a >= f + 1 ] (?, 1) f25(a, b, c, d, e, f, g, h) -> f25(a, b, c, d, e, f, i, h + 1) [ e >= h + 1 ] (?, 1) f41(a, b, c, d, e, f, g, h) -> f15(a, b, c, d, e, f + 1, g, h) [ e >= b ] (?, 1) f41(a, b, c, d, e, f, g, h) -> f15(a, b, c, d, e + 1, f + 1, g, h) [ b >= e + 1 ] (?, 1) f25(a, b, c, d, e, f, g, h) -> f41(a, b, c, d, e, f, g, h) [ h >= e /\ i >= j + 1 ] (?, 1) f25(a, b, c, d, e, f, g, h) -> f41(a, b, c, d, e, f, g, h) [ h >= e ] (?, 1) f25(a, b, c, d, e, f, g, h) -> f15(a, b, c, d, e - 1, f + 1, g, h) [ h >= e ] (?, 1) f15(a, b, c, d, e, f, g, h) -> f48(a, b, c, d, e, f, g, h) [ f >= a ] start location: f0 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, e, f, h]. We thus obtain the following problem: 2: T: (?, 1) f15(a, b, e, f, h) -> f48(a, b, e, f, h) [ f >= a ] (?, 1) f25(a, b, e, f, h) -> f15(a, b, e - 1, f + 1, h) [ h >= e ] (?, 1) f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e ] (?, 1) f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e /\ i >= j + 1 ] (?, 1) f41(a, b, e, f, h) -> f15(a, b, e + 1, f + 1, h) [ b >= e + 1 ] (?, 1) f41(a, b, e, f, h) -> f15(a, b, e, f + 1, h) [ e >= b ] (?, 1) f25(a, b, e, f, h) -> f25(a, b, e, f, h + 1) [ e >= h + 1 ] (?, 1) f15(a, b, e, f, h) -> f25(a, b, e, f, 1) [ a >= f + 1 ] (1, 1) f0(a, b, e, f, h) -> f15(10, 35, i, 0, h) start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (?, 1) f25(a, b, e, f, h) -> f15(a, b, e - 1, f + 1, h) [ h >= e ] (?, 1) f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e ] (?, 1) f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e /\ i >= j + 1 ] (?, 1) f41(a, b, e, f, h) -> f15(a, b, e + 1, f + 1, h) [ b >= e + 1 ] (?, 1) f41(a, b, e, f, h) -> f15(a, b, e, f + 1, h) [ e >= b ] (?, 1) f25(a, b, e, f, h) -> f25(a, b, e, f, h + 1) [ e >= h + 1 ] (?, 1) f15(a, b, e, f, h) -> f25(a, b, e, f, 1) [ a >= f + 1 ] (1, 1) f0(a, b, e, f, h) -> f15(10, 35, i, 0, h) start location: f0 leaf cost: 1 A polynomial rank function with Pol(f25) = 3*V_1 - 3*V_4 - 1 Pol(f15) = 3*V_1 - 3*V_4 Pol(f41) = 3*V_1 - 3*V_4 - 2 Pol(f0) = 30 orients all transitions weakly and the transition f15(a, b, e, f, h) -> f25(a, b, e, f, 1) [ a >= f + 1 ] strictly and produces the following problem: 4: T: (?, 1) f25(a, b, e, f, h) -> f15(a, b, e - 1, f + 1, h) [ h >= e ] (?, 1) f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e ] (?, 1) f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e /\ i >= j + 1 ] (?, 1) f41(a, b, e, f, h) -> f15(a, b, e + 1, f + 1, h) [ b >= e + 1 ] (?, 1) f41(a, b, e, f, h) -> f15(a, b, e, f + 1, h) [ e >= b ] (?, 1) f25(a, b, e, f, h) -> f25(a, b, e, f, h + 1) [ e >= h + 1 ] (30, 1) f15(a, b, e, f, h) -> f25(a, b, e, f, 1) [ a >= f + 1 ] (1, 1) f0(a, b, e, f, h) -> f15(10, 35, i, 0, h) start location: f0 leaf cost: 1 A polynomial rank function with Pol(f41) = 1 Pol(f15) = 0 Pol(f25) = 2 and size complexities S("f0(a, b, e, f, h) -> f15(10, 35, i, 0, h)", 0-0) = 10 S("f0(a, b, e, f, h) -> f15(10, 35, i, 0, h)", 0-1) = 35 S("f0(a, b, e, f, h) -> f15(10, 35, i, 0, h)", 0-2) = ? S("f0(a, b, e, f, h) -> f15(10, 35, i, 0, h)", 0-3) = 0 S("f0(a, b, e, f, h) -> f15(10, 35, i, 0, h)", 0-4) = h S("f15(a, b, e, f, h) -> f25(a, b, e, f, 1) [ a >= f + 1 ]", 0-0) = 10 S("f15(a, b, e, f, h) -> f25(a, b, e, f, 1) [ a >= f + 1 ]", 0-1) = 35 S("f15(a, b, e, f, h) -> f25(a, b, e, f, 1) [ a >= f + 1 ]", 0-2) = ? S("f15(a, b, e, f, h) -> f25(a, b, e, f, 1) [ a >= f + 1 ]", 0-3) = ? S("f15(a, b, e, f, h) -> f25(a, b, e, f, 1) [ a >= f + 1 ]", 0-4) = 1 S("f25(a, b, e, f, h) -> f25(a, b, e, f, h + 1) [ e >= h + 1 ]", 0-0) = 10 S("f25(a, b, e, f, h) -> f25(a, b, e, f, h + 1) [ e >= h + 1 ]", 0-1) = 35 S("f25(a, b, e, f, h) -> f25(a, b, e, f, h + 1) [ e >= h + 1 ]", 0-2) = ? S("f25(a, b, e, f, h) -> f25(a, b, e, f, h + 1) [ e >= h + 1 ]", 0-3) = ? S("f25(a, b, e, f, h) -> f25(a, b, e, f, h + 1) [ e >= h + 1 ]", 0-4) = ? S("f41(a, b, e, f, h) -> f15(a, b, e, f + 1, h) [ e >= b ]", 0-0) = 10 S("f41(a, b, e, f, h) -> f15(a, b, e, f + 1, h) [ e >= b ]", 0-1) = 35 S("f41(a, b, e, f, h) -> f15(a, b, e, f + 1, h) [ e >= b ]", 0-2) = ? S("f41(a, b, e, f, h) -> f15(a, b, e, f + 1, h) [ e >= b ]", 0-3) = ? S("f41(a, b, e, f, h) -> f15(a, b, e, f + 1, h) [ e >= b ]", 0-4) = ? S("f41(a, b, e, f, h) -> f15(a, b, e + 1, f + 1, h) [ b >= e + 1 ]", 0-0) = 10 S("f41(a, b, e, f, h) -> f15(a, b, e + 1, f + 1, h) [ b >= e + 1 ]", 0-1) = 35 S("f41(a, b, e, f, h) -> f15(a, b, e + 1, f + 1, h) [ b >= e + 1 ]", 0-2) = ? S("f41(a, b, e, f, h) -> f15(a, b, e + 1, f + 1, h) [ b >= e + 1 ]", 0-3) = ? S("f41(a, b, e, f, h) -> f15(a, b, e + 1, f + 1, h) [ b >= e + 1 ]", 0-4) = ? S("f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e /\\ i >= j + 1 ]", 0-0) = 10 S("f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e /\\ i >= j + 1 ]", 0-1) = 35 S("f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e /\\ i >= j + 1 ]", 0-2) = ? S("f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e /\\ i >= j + 1 ]", 0-3) = ? S("f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e /\\ i >= j + 1 ]", 0-4) = ? S("f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e ]", 0-0) = 10 S("f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e ]", 0-1) = 35 S("f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e ]", 0-2) = ? S("f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e ]", 0-3) = ? S("f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e ]", 0-4) = ? S("f25(a, b, e, f, h) -> f15(a, b, e - 1, f + 1, h) [ h >= e ]", 0-0) = 10 S("f25(a, b, e, f, h) -> f15(a, b, e - 1, f + 1, h) [ h >= e ]", 0-1) = 35 S("f25(a, b, e, f, h) -> f15(a, b, e - 1, f + 1, h) [ h >= e ]", 0-2) = ? S("f25(a, b, e, f, h) -> f15(a, b, e - 1, f + 1, h) [ h >= e ]", 0-3) = ? S("f25(a, b, e, f, h) -> f15(a, b, e - 1, f + 1, h) [ h >= e ]", 0-4) = ? orients the transitions f41(a, b, e, f, h) -> f15(a, b, e + 1, f + 1, h) [ b >= e + 1 ] f41(a, b, e, f, h) -> f15(a, b, e, f + 1, h) [ e >= b ] f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e /\ i >= j + 1 ] f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e ] f25(a, b, e, f, h) -> f25(a, b, e, f, h + 1) [ e >= h + 1 ] f25(a, b, e, f, h) -> f15(a, b, e - 1, f + 1, h) [ h >= e ] weakly and the transitions f41(a, b, e, f, h) -> f15(a, b, e + 1, f + 1, h) [ b >= e + 1 ] f41(a, b, e, f, h) -> f15(a, b, e, f + 1, h) [ e >= b ] f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e /\ i >= j + 1 ] f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e ] f25(a, b, e, f, h) -> f15(a, b, e - 1, f + 1, h) [ h >= e ] strictly and produces the following problem: 5: T: (60, 1) f25(a, b, e, f, h) -> f15(a, b, e - 1, f + 1, h) [ h >= e ] (60, 1) f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e ] (60, 1) f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e /\ i >= j + 1 ] (60, 1) f41(a, b, e, f, h) -> f15(a, b, e + 1, f + 1, h) [ b >= e + 1 ] (60, 1) f41(a, b, e, f, h) -> f15(a, b, e, f + 1, h) [ e >= b ] (?, 1) f25(a, b, e, f, h) -> f25(a, b, e, f, h + 1) [ e >= h + 1 ] (30, 1) f15(a, b, e, f, h) -> f25(a, b, e, f, 1) [ a >= f + 1 ] (1, 1) f0(a, b, e, f, h) -> f15(10, 35, i, 0, h) start location: f0 leaf cost: 1 By chaining the transition f25(a, b, e, f, h) -> f15(a, b, e - 1, f + 1, h) [ h >= e ] with all transitions in problem 5, the following new transition is obtained: f25(a, b, e, f, h) -> f25(a, b, e - 1, f + 1, 1) [ h >= e /\ a >= f + 2 ] We thus obtain the following problem: 6: T: (60, 2) f25(a, b, e, f, h) -> f25(a, b, e - 1, f + 1, 1) [ h >= e /\ a >= f + 2 ] (60, 1) f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e ] (60, 1) f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e /\ i >= j + 1 ] (60, 1) f41(a, b, e, f, h) -> f15(a, b, e + 1, f + 1, h) [ b >= e + 1 ] (60, 1) f41(a, b, e, f, h) -> f15(a, b, e, f + 1, h) [ e >= b ] (?, 1) f25(a, b, e, f, h) -> f25(a, b, e, f, h + 1) [ e >= h + 1 ] (30, 1) f15(a, b, e, f, h) -> f25(a, b, e, f, 1) [ a >= f + 1 ] (1, 1) f0(a, b, e, f, h) -> f15(10, 35, i, 0, h) start location: f0 leaf cost: 1 By chaining the transition f41(a, b, e, f, h) -> f15(a, b, e + 1, f + 1, h) [ b >= e + 1 ] with all transitions in problem 6, the following new transition is obtained: f41(a, b, e, f, h) -> f25(a, b, e + 1, f + 1, 1) [ b >= e + 1 /\ a >= f + 2 ] We thus obtain the following problem: 7: T: (60, 2) f41(a, b, e, f, h) -> f25(a, b, e + 1, f + 1, 1) [ b >= e + 1 /\ a >= f + 2 ] (60, 2) f25(a, b, e, f, h) -> f25(a, b, e - 1, f + 1, 1) [ h >= e /\ a >= f + 2 ] (60, 1) f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e ] (60, 1) f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e /\ i >= j + 1 ] (60, 1) f41(a, b, e, f, h) -> f15(a, b, e, f + 1, h) [ e >= b ] (?, 1) f25(a, b, e, f, h) -> f25(a, b, e, f, h + 1) [ e >= h + 1 ] (30, 1) f15(a, b, e, f, h) -> f25(a, b, e, f, 1) [ a >= f + 1 ] (1, 1) f0(a, b, e, f, h) -> f15(10, 35, i, 0, h) start location: f0 leaf cost: 1 By chaining the transition f41(a, b, e, f, h) -> f15(a, b, e, f + 1, h) [ e >= b ] with all transitions in problem 7, the following new transition is obtained: f41(a, b, e, f, h) -> f25(a, b, e, f + 1, 1) [ e >= b /\ a >= f + 2 ] We thus obtain the following problem: 8: T: (60, 2) f41(a, b, e, f, h) -> f25(a, b, e, f + 1, 1) [ e >= b /\ a >= f + 2 ] (60, 2) f41(a, b, e, f, h) -> f25(a, b, e + 1, f + 1, 1) [ b >= e + 1 /\ a >= f + 2 ] (60, 2) f25(a, b, e, f, h) -> f25(a, b, e - 1, f + 1, 1) [ h >= e /\ a >= f + 2 ] (60, 1) f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e ] (60, 1) f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e /\ i >= j + 1 ] (?, 1) f25(a, b, e, f, h) -> f25(a, b, e, f, h + 1) [ e >= h + 1 ] (30, 1) f15(a, b, e, f, h) -> f25(a, b, e, f, 1) [ a >= f + 1 ] (1, 1) f0(a, b, e, f, h) -> f15(10, 35, i, 0, h) start location: f0 leaf cost: 1 By chaining the transition f0(a, b, e, f, h) -> f15(10, 35, i, 0, h) with all transitions in problem 8, the following new transition is obtained: f0(a, b, e, f, h) -> f25(10, 35, i, 0, 1) [ 10 >= 1 ] We thus obtain the following problem: 9: T: (1, 2) f0(a, b, e, f, h) -> f25(10, 35, i, 0, 1) [ 10 >= 1 ] (60, 2) f41(a, b, e, f, h) -> f25(a, b, e, f + 1, 1) [ e >= b /\ a >= f + 2 ] (60, 2) f41(a, b, e, f, h) -> f25(a, b, e + 1, f + 1, 1) [ b >= e + 1 /\ a >= f + 2 ] (60, 2) f25(a, b, e, f, h) -> f25(a, b, e - 1, f + 1, 1) [ h >= e /\ a >= f + 2 ] (60, 1) f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e ] (60, 1) f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e /\ i >= j + 1 ] (?, 1) f25(a, b, e, f, h) -> f25(a, b, e, f, h + 1) [ e >= h + 1 ] (30, 1) f15(a, b, e, f, h) -> f25(a, b, e, f, 1) [ a >= f + 1 ] start location: f0 leaf cost: 1 Testing for reachability in the complexity graph removes the following transition from problem 9: f15(a, b, e, f, h) -> f25(a, b, e, f, 1) [ a >= f + 1 ] We thus obtain the following problem: 10: T: (60, 2) f41(a, b, e, f, h) -> f25(a, b, e, f + 1, 1) [ e >= b /\ a >= f + 2 ] (60, 2) f41(a, b, e, f, h) -> f25(a, b, e + 1, f + 1, 1) [ b >= e + 1 /\ a >= f + 2 ] (60, 2) f25(a, b, e, f, h) -> f25(a, b, e - 1, f + 1, 1) [ h >= e /\ a >= f + 2 ] (?, 1) f25(a, b, e, f, h) -> f25(a, b, e, f, h + 1) [ e >= h + 1 ] (60, 1) f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e /\ i >= j + 1 ] (60, 1) f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e ] (1, 2) f0(a, b, e, f, h) -> f25(10, 35, i, 0, 1) [ 10 >= 1 ] start location: f0 leaf cost: 1 By chaining the transition f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e /\ i >= j + 1 ] with all transitions in problem 10, the following new transitions are obtained: f25(a, b, e, f, h) -> f25(a, b, e, f + 1, 1) [ h >= e /\ i >= j + 1 /\ e >= b /\ a >= f + 2 ] f25(a, b, e, f, h) -> f25(a, b, e + 1, f + 1, 1) [ h >= e /\ i >= j + 1 /\ b >= e + 1 /\ a >= f + 2 ] We thus obtain the following problem: 11: T: (60, 3) f25(a, b, e, f, h) -> f25(a, b, e, f + 1, 1) [ h >= e /\ i >= j + 1 /\ e >= b /\ a >= f + 2 ] (60, 3) f25(a, b, e, f, h) -> f25(a, b, e + 1, f + 1, 1) [ h >= e /\ i >= j + 1 /\ b >= e + 1 /\ a >= f + 2 ] (60, 2) f41(a, b, e, f, h) -> f25(a, b, e, f + 1, 1) [ e >= b /\ a >= f + 2 ] (60, 2) f41(a, b, e, f, h) -> f25(a, b, e + 1, f + 1, 1) [ b >= e + 1 /\ a >= f + 2 ] (60, 2) f25(a, b, e, f, h) -> f25(a, b, e - 1, f + 1, 1) [ h >= e /\ a >= f + 2 ] (?, 1) f25(a, b, e, f, h) -> f25(a, b, e, f, h + 1) [ e >= h + 1 ] (60, 1) f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e ] (1, 2) f0(a, b, e, f, h) -> f25(10, 35, i, 0, 1) [ 10 >= 1 ] start location: f0 leaf cost: 1 By chaining the transition f25(a, b, e, f, h) -> f41(a, b, e, f, h) [ h >= e ] with all transitions in problem 11, the following new transitions are obtained: f25(a, b, e, f, h) -> f25(a, b, e, f + 1, 1) [ h >= e /\ e >= b /\ a >= f + 2 ] f25(a, b, e, f, h) -> f25(a, b, e + 1, f + 1, 1) [ h >= e /\ b >= e + 1 /\ a >= f + 2 ] We thus obtain the following problem: 12: T: (60, 3) f25(a, b, e, f, h) -> f25(a, b, e, f + 1, 1) [ h >= e /\ e >= b /\ a >= f + 2 ] (60, 3) f25(a, b, e, f, h) -> f25(a, b, e + 1, f + 1, 1) [ h >= e /\ b >= e + 1 /\ a >= f + 2 ] (60, 3) f25(a, b, e, f, h) -> f25(a, b, e, f + 1, 1) [ h >= e /\ i >= j + 1 /\ e >= b /\ a >= f + 2 ] (60, 3) f25(a, b, e, f, h) -> f25(a, b, e + 1, f + 1, 1) [ h >= e /\ i >= j + 1 /\ b >= e + 1 /\ a >= f + 2 ] (60, 2) f41(a, b, e, f, h) -> f25(a, b, e, f + 1, 1) [ e >= b /\ a >= f + 2 ] (60, 2) f41(a, b, e, f, h) -> f25(a, b, e + 1, f + 1, 1) [ b >= e + 1 /\ a >= f + 2 ] (60, 2) f25(a, b, e, f, h) -> f25(a, b, e - 1, f + 1, 1) [ h >= e /\ a >= f + 2 ] (?, 1) f25(a, b, e, f, h) -> f25(a, b, e, f, h + 1) [ e >= h + 1 ] (1, 2) f0(a, b, e, f, h) -> f25(10, 35, i, 0, 1) [ 10 >= 1 ] start location: f0 leaf cost: 1 Testing for reachability in the complexity graph removes the following transitions from problem 12: f41(a, b, e, f, h) -> f25(a, b, e, f + 1, 1) [ e >= b /\ a >= f + 2 ] f41(a, b, e, f, h) -> f25(a, b, e + 1, f + 1, 1) [ b >= e + 1 /\ a >= f + 2 ] We thus obtain the following problem: 13: T: (60, 3) f25(a, b, e, f, h) -> f25(a, b, e, f + 1, 1) [ h >= e /\ e >= b /\ a >= f + 2 ] (60, 3) f25(a, b, e, f, h) -> f25(a, b, e, f + 1, 1) [ h >= e /\ i >= j + 1 /\ e >= b /\ a >= f + 2 ] (60, 3) f25(a, b, e, f, h) -> f25(a, b, e + 1, f + 1, 1) [ h >= e /\ b >= e + 1 /\ a >= f + 2 ] (60, 3) f25(a, b, e, f, h) -> f25(a, b, e + 1, f + 1, 1) [ h >= e /\ i >= j + 1 /\ b >= e + 1 /\ a >= f + 2 ] (60, 2) f25(a, b, e, f, h) -> f25(a, b, e - 1, f + 1, 1) [ h >= e /\ a >= f + 2 ] (?, 1) f25(a, b, e, f, h) -> f25(a, b, e, f, h + 1) [ e >= h + 1 ] (1, 2) f0(a, b, e, f, h) -> f25(10, 35, i, 0, 1) [ 10 >= 1 ] start location: f0 leaf cost: 1 Complexity upper bound ? Time: 3.759 sec (SMT: 3.486 sec)