MAYBE Initial complexity problem: 1: T: (1, 1) f0(a, b) -> f4(0, 99) (?, 1) f4(a, b) -> f4(e, b) [ b >= a + 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(a, e) [ b >= a + 1 ] (?, 1) f4(a, b) -> f11(a, b) [ a >= b ] start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem: 2: T: (1, 1) f0(a, b) -> f4(0, 99) (?, 1) f4(a, b) -> f4(e, b) [ b >= a + 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(a, e) [ b >= a + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b) -> f4(0, 99) with all transitions in problem 2, the following new transitions are obtained: f0(a, b) -> f4(0, e) [ 99 >= 1 ] f0(a, b) -> f4(e, 99) [ 99 >= 1 /\ c >= d + 1 ] We thus obtain the following problem: 3: T: (1, 2) f0(a, b) -> f4(0, e) [ 99 >= 1 ] (1, 2) f0(a, b) -> f4(e, 99) [ 99 >= 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(e, b) [ b >= a + 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(a, e) [ b >= a + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b) -> f4(0, e) [ 99 >= 1 ] with all transitions in problem 3, the following new transitions are obtained: f0(a, b) -> f4(0, e') [ 99 >= 1 /\ e >= 1 ] f0(a, b) -> f4(e', e) [ 99 >= 1 /\ e >= 1 /\ c >= d + 1 ] We thus obtain the following problem: 4: T: (1, 3) f0(a, b) -> f4(0, e') [ 99 >= 1 /\ e >= 1 ] (1, 3) f0(a, b) -> f4(e', e) [ 99 >= 1 /\ e >= 1 /\ c >= d + 1 ] (1, 2) f0(a, b) -> f4(e, 99) [ 99 >= 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(e, b) [ b >= a + 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(a, e) [ b >= a + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b) -> f4(0, e') [ 99 >= 1 /\ e >= 1 ] with all transitions in problem 4, the following new transitions are obtained: f0(a, b) -> f4(0, e'') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 ] f0(a, b) -> f4(e'', e') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ c >= d + 1 ] We thus obtain the following problem: 5: T: (1, 4) f0(a, b) -> f4(0, e'') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 ] (1, 4) f0(a, b) -> f4(e'', e') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ c >= d + 1 ] (1, 3) f0(a, b) -> f4(e', e) [ 99 >= 1 /\ e >= 1 /\ c >= d + 1 ] (1, 2) f0(a, b) -> f4(e, 99) [ 99 >= 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(e, b) [ b >= a + 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(a, e) [ b >= a + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b) -> f4(0, e'') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 ] with all transitions in problem 5, the following new transitions are obtained: f0(a, b) -> f4(0, e''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 ] f0(a, b) -> f4(e''', e'') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ c >= d + 1 ] We thus obtain the following problem: 6: T: (1, 5) f0(a, b) -> f4(0, e''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 ] (1, 5) f0(a, b) -> f4(e''', e'') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ c >= d + 1 ] (1, 4) f0(a, b) -> f4(e'', e') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ c >= d + 1 ] (1, 3) f0(a, b) -> f4(e', e) [ 99 >= 1 /\ e >= 1 /\ c >= d + 1 ] (1, 2) f0(a, b) -> f4(e, 99) [ 99 >= 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(e, b) [ b >= a + 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(a, e) [ b >= a + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b) -> f4(0, e''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 ] with all transitions in problem 6, the following new transitions are obtained: f0(a, b) -> f4(0, e'''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 ] f0(a, b) -> f4(e'''', e''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ c >= d + 1 ] We thus obtain the following problem: 7: T: (1, 6) f0(a, b) -> f4(0, e'''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 ] (1, 6) f0(a, b) -> f4(e'''', e''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ c >= d + 1 ] (1, 5) f0(a, b) -> f4(e''', e'') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ c >= d + 1 ] (1, 4) f0(a, b) -> f4(e'', e') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ c >= d + 1 ] (1, 3) f0(a, b) -> f4(e', e) [ 99 >= 1 /\ e >= 1 /\ c >= d + 1 ] (1, 2) f0(a, b) -> f4(e, 99) [ 99 >= 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(e, b) [ b >= a + 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(a, e) [ b >= a + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b) -> f4(0, e'''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 ] with all transitions in problem 7, the following new transitions are obtained: f0(a, b) -> f4(0, e''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 ] f0(a, b) -> f4(e''''', e'''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ c >= d + 1 ] We thus obtain the following problem: 8: T: (1, 7) f0(a, b) -> f4(0, e''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 ] (1, 7) f0(a, b) -> f4(e''''', e'''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ c >= d + 1 ] (1, 6) f0(a, b) -> f4(e'''', e''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ c >= d + 1 ] (1, 5) f0(a, b) -> f4(e''', e'') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ c >= d + 1 ] (1, 4) f0(a, b) -> f4(e'', e') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ c >= d + 1 ] (1, 3) f0(a, b) -> f4(e', e) [ 99 >= 1 /\ e >= 1 /\ c >= d + 1 ] (1, 2) f0(a, b) -> f4(e, 99) [ 99 >= 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(e, b) [ b >= a + 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(a, e) [ b >= a + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b) -> f4(0, e''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 ] with all transitions in problem 8, the following new transitions are obtained: f0(a, b) -> f4(0, e'''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 ] f0(a, b) -> f4(e'''''', e''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ c >= d + 1 ] We thus obtain the following problem: 9: T: (1, 8) f0(a, b) -> f4(0, e'''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 ] (1, 8) f0(a, b) -> f4(e'''''', e''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ c >= d + 1 ] (1, 7) f0(a, b) -> f4(e''''', e'''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ c >= d + 1 ] (1, 6) f0(a, b) -> f4(e'''', e''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ c >= d + 1 ] (1, 5) f0(a, b) -> f4(e''', e'') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ c >= d + 1 ] (1, 4) f0(a, b) -> f4(e'', e') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ c >= d + 1 ] (1, 3) f0(a, b) -> f4(e', e) [ 99 >= 1 /\ e >= 1 /\ c >= d + 1 ] (1, 2) f0(a, b) -> f4(e, 99) [ 99 >= 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(e, b) [ b >= a + 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(a, e) [ b >= a + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b) -> f4(0, e'''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 ] with all transitions in problem 9, the following new transitions are obtained: f0(a, b) -> f4(0, e''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 ] f0(a, b) -> f4(e''''''', e'''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ c >= d + 1 ] We thus obtain the following problem: 10: T: (1, 9) f0(a, b) -> f4(0, e''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 ] (1, 9) f0(a, b) -> f4(e''''''', e'''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ c >= d + 1 ] (1, 8) f0(a, b) -> f4(e'''''', e''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ c >= d + 1 ] (1, 7) f0(a, b) -> f4(e''''', e'''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ c >= d + 1 ] (1, 6) f0(a, b) -> f4(e'''', e''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ c >= d + 1 ] (1, 5) f0(a, b) -> f4(e''', e'') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ c >= d + 1 ] (1, 4) f0(a, b) -> f4(e'', e') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ c >= d + 1 ] (1, 3) f0(a, b) -> f4(e', e) [ 99 >= 1 /\ e >= 1 /\ c >= d + 1 ] (1, 2) f0(a, b) -> f4(e, 99) [ 99 >= 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(e, b) [ b >= a + 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(a, e) [ b >= a + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b) -> f4(0, e''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 ] with all transitions in problem 10, the following new transitions are obtained: f0(a, b) -> f4(0, e'''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 ] f0(a, b) -> f4(e'''''''', e''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ c >= d + 1 ] We thus obtain the following problem: 11: T: (1, 10) f0(a, b) -> f4(0, e'''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 ] (1, 10) f0(a, b) -> f4(e'''''''', e''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ c >= d + 1 ] (1, 9) f0(a, b) -> f4(e''''''', e'''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ c >= d + 1 ] (1, 8) f0(a, b) -> f4(e'''''', e''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ c >= d + 1 ] (1, 7) f0(a, b) -> f4(e''''', e'''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ c >= d + 1 ] (1, 6) f0(a, b) -> f4(e'''', e''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ c >= d + 1 ] (1, 5) f0(a, b) -> f4(e''', e'') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ c >= d + 1 ] (1, 4) f0(a, b) -> f4(e'', e') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ c >= d + 1 ] (1, 3) f0(a, b) -> f4(e', e) [ 99 >= 1 /\ e >= 1 /\ c >= d + 1 ] (1, 2) f0(a, b) -> f4(e, 99) [ 99 >= 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(e, b) [ b >= a + 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(a, e) [ b >= a + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b) -> f4(0, e'''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 ] with all transitions in problem 11, the following new transitions are obtained: f0(a, b) -> f4(0, e''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 ] f0(a, b) -> f4(e''''''''', e'''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ c >= d + 1 ] We thus obtain the following problem: 12: T: (1, 11) f0(a, b) -> f4(0, e''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 ] (1, 11) f0(a, b) -> f4(e''''''''', e'''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ c >= d + 1 ] (1, 10) f0(a, b) -> f4(e'''''''', e''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ c >= d + 1 ] (1, 9) f0(a, b) -> f4(e''''''', e'''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ c >= d + 1 ] (1, 8) f0(a, b) -> f4(e'''''', e''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ c >= d + 1 ] (1, 7) f0(a, b) -> f4(e''''', e'''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ c >= d + 1 ] (1, 6) f0(a, b) -> f4(e'''', e''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ c >= d + 1 ] (1, 5) f0(a, b) -> f4(e''', e'') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ c >= d + 1 ] (1, 4) f0(a, b) -> f4(e'', e') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ c >= d + 1 ] (1, 3) f0(a, b) -> f4(e', e) [ 99 >= 1 /\ e >= 1 /\ c >= d + 1 ] (1, 2) f0(a, b) -> f4(e, 99) [ 99 >= 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(e, b) [ b >= a + 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(a, e) [ b >= a + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b) -> f4(0, e''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 ] with all transitions in problem 12, the following new transitions are obtained: f0(a, b) -> f4(0, e'''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 ] f0(a, b) -> f4(e'''''''''', e''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ c >= d + 1 ] We thus obtain the following problem: 13: T: (1, 12) f0(a, b) -> f4(0, e'''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 ] (1, 12) f0(a, b) -> f4(e'''''''''', e''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ c >= d + 1 ] (1, 11) f0(a, b) -> f4(e''''''''', e'''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ c >= d + 1 ] (1, 10) f0(a, b) -> f4(e'''''''', e''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ c >= d + 1 ] (1, 9) f0(a, b) -> f4(e''''''', e'''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ c >= d + 1 ] (1, 8) f0(a, b) -> f4(e'''''', e''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ c >= d + 1 ] (1, 7) f0(a, b) -> f4(e''''', e'''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ c >= d + 1 ] (1, 6) f0(a, b) -> f4(e'''', e''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ c >= d + 1 ] (1, 5) f0(a, b) -> f4(e''', e'') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ c >= d + 1 ] (1, 4) f0(a, b) -> f4(e'', e') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ c >= d + 1 ] (1, 3) f0(a, b) -> f4(e', e) [ 99 >= 1 /\ e >= 1 /\ c >= d + 1 ] (1, 2) f0(a, b) -> f4(e, 99) [ 99 >= 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(e, b) [ b >= a + 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(a, e) [ b >= a + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b) -> f4(0, e'''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 ] with all transitions in problem 13, the following new transitions are obtained: f0(a, b) -> f4(0, e''''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 ] f0(a, b) -> f4(e''''''''''', e'''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 /\ c >= d + 1 ] We thus obtain the following problem: 14: T: (1, 13) f0(a, b) -> f4(0, e''''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 ] (1, 13) f0(a, b) -> f4(e''''''''''', e'''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 /\ c >= d + 1 ] (1, 12) f0(a, b) -> f4(e'''''''''', e''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ c >= d + 1 ] (1, 11) f0(a, b) -> f4(e''''''''', e'''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ c >= d + 1 ] (1, 10) f0(a, b) -> f4(e'''''''', e''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ c >= d + 1 ] (1, 9) f0(a, b) -> f4(e''''''', e'''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ c >= d + 1 ] (1, 8) f0(a, b) -> f4(e'''''', e''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ c >= d + 1 ] (1, 7) f0(a, b) -> f4(e''''', e'''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ c >= d + 1 ] (1, 6) f0(a, b) -> f4(e'''', e''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ c >= d + 1 ] (1, 5) f0(a, b) -> f4(e''', e'') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ c >= d + 1 ] (1, 4) f0(a, b) -> f4(e'', e') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ c >= d + 1 ] (1, 3) f0(a, b) -> f4(e', e) [ 99 >= 1 /\ e >= 1 /\ c >= d + 1 ] (1, 2) f0(a, b) -> f4(e, 99) [ 99 >= 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(e, b) [ b >= a + 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(a, e) [ b >= a + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b) -> f4(0, e''''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 ] with all transitions in problem 14, the following new transitions are obtained: f0(a, b) -> f4(0, e'''''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 /\ e''''''''''' >= 1 ] f0(a, b) -> f4(e'''''''''''', e''''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 /\ e''''''''''' >= 1 /\ c >= d + 1 ] We thus obtain the following problem: 15: T: (1, 14) f0(a, b) -> f4(0, e'''''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 /\ e''''''''''' >= 1 ] (1, 14) f0(a, b) -> f4(e'''''''''''', e''''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 /\ e''''''''''' >= 1 /\ c >= d + 1 ] (1, 13) f0(a, b) -> f4(e''''''''''', e'''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 /\ c >= d + 1 ] (1, 12) f0(a, b) -> f4(e'''''''''', e''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ c >= d + 1 ] (1, 11) f0(a, b) -> f4(e''''''''', e'''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ c >= d + 1 ] (1, 10) f0(a, b) -> f4(e'''''''', e''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ c >= d + 1 ] (1, 9) f0(a, b) -> f4(e''''''', e'''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ c >= d + 1 ] (1, 8) f0(a, b) -> f4(e'''''', e''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ c >= d + 1 ] (1, 7) f0(a, b) -> f4(e''''', e'''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ c >= d + 1 ] (1, 6) f0(a, b) -> f4(e'''', e''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ c >= d + 1 ] (1, 5) f0(a, b) -> f4(e''', e'') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ c >= d + 1 ] (1, 4) f0(a, b) -> f4(e'', e') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ c >= d + 1 ] (1, 3) f0(a, b) -> f4(e', e) [ 99 >= 1 /\ e >= 1 /\ c >= d + 1 ] (1, 2) f0(a, b) -> f4(e, 99) [ 99 >= 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(e, b) [ b >= a + 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(a, e) [ b >= a + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b) -> f4(0, e'''''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 /\ e''''''''''' >= 1 ] with all transitions in problem 15, the following new transitions are obtained: f0(a, b) -> f4(0, e''''''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 /\ e''''''''''' >= 1 /\ e'''''''''''' >= 1 ] f0(a, b) -> f4(e''''''''''''', e'''''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 /\ e''''''''''' >= 1 /\ e'''''''''''' >= 1 /\ c >= d + 1 ] We thus obtain the following problem: 16: T: (1, 15) f0(a, b) -> f4(0, e''''''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 /\ e''''''''''' >= 1 /\ e'''''''''''' >= 1 ] (1, 15) f0(a, b) -> f4(e''''''''''''', e'''''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 /\ e''''''''''' >= 1 /\ e'''''''''''' >= 1 /\ c >= d + 1 ] (1, 14) f0(a, b) -> f4(e'''''''''''', e''''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 /\ e''''''''''' >= 1 /\ c >= d + 1 ] (1, 13) f0(a, b) -> f4(e''''''''''', e'''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 /\ c >= d + 1 ] (1, 12) f0(a, b) -> f4(e'''''''''', e''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ c >= d + 1 ] (1, 11) f0(a, b) -> f4(e''''''''', e'''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ c >= d + 1 ] (1, 10) f0(a, b) -> f4(e'''''''', e''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ c >= d + 1 ] (1, 9) f0(a, b) -> f4(e''''''', e'''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ c >= d + 1 ] (1, 8) f0(a, b) -> f4(e'''''', e''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ c >= d + 1 ] (1, 7) f0(a, b) -> f4(e''''', e'''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ c >= d + 1 ] (1, 6) f0(a, b) -> f4(e'''', e''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ c >= d + 1 ] (1, 5) f0(a, b) -> f4(e''', e'') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ c >= d + 1 ] (1, 4) f0(a, b) -> f4(e'', e') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ c >= d + 1 ] (1, 3) f0(a, b) -> f4(e', e) [ 99 >= 1 /\ e >= 1 /\ c >= d + 1 ] (1, 2) f0(a, b) -> f4(e, 99) [ 99 >= 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(e, b) [ b >= a + 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(a, e) [ b >= a + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b) -> f4(0, e''''''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 /\ e''''''''''' >= 1 /\ e'''''''''''' >= 1 ] with all transitions in problem 16, the following new transitions are obtained: f0(a, b) -> f4(0, e'''''''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 /\ e''''''''''' >= 1 /\ e'''''''''''' >= 1 /\ e''''''''''''' >= 1 ] f0(a, b) -> f4(e'''''''''''''', e''''''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 /\ e''''''''''' >= 1 /\ e'''''''''''' >= 1 /\ e''''''''''''' >= 1 /\ c >= d + 1 ] We thus obtain the following problem: 17: T: (1, 16) f0(a, b) -> f4(0, e'''''''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 /\ e''''''''''' >= 1 /\ e'''''''''''' >= 1 /\ e''''''''''''' >= 1 ] (1, 16) f0(a, b) -> f4(e'''''''''''''', e''''''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 /\ e''''''''''' >= 1 /\ e'''''''''''' >= 1 /\ e''''''''''''' >= 1 /\ c >= d + 1 ] (1, 15) f0(a, b) -> f4(e''''''''''''', e'''''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 /\ e''''''''''' >= 1 /\ e'''''''''''' >= 1 /\ c >= d + 1 ] (1, 14) f0(a, b) -> f4(e'''''''''''', e''''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 /\ e''''''''''' >= 1 /\ c >= d + 1 ] (1, 13) f0(a, b) -> f4(e''''''''''', e'''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ e'''''''''' >= 1 /\ c >= d + 1 ] (1, 12) f0(a, b) -> f4(e'''''''''', e''''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ e''''''''' >= 1 /\ c >= d + 1 ] (1, 11) f0(a, b) -> f4(e''''''''', e'''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ e'''''''' >= 1 /\ c >= d + 1 ] (1, 10) f0(a, b) -> f4(e'''''''', e''''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ e''''''' >= 1 /\ c >= d + 1 ] (1, 9) f0(a, b) -> f4(e''''''', e'''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ e'''''' >= 1 /\ c >= d + 1 ] (1, 8) f0(a, b) -> f4(e'''''', e''''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ e''''' >= 1 /\ c >= d + 1 ] (1, 7) f0(a, b) -> f4(e''''', e'''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ e'''' >= 1 /\ c >= d + 1 ] (1, 6) f0(a, b) -> f4(e'''', e''') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ e''' >= 1 /\ c >= d + 1 ] (1, 5) f0(a, b) -> f4(e''', e'') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ e'' >= 1 /\ c >= d + 1 ] (1, 4) f0(a, b) -> f4(e'', e') [ 99 >= 1 /\ e >= 1 /\ e' >= 1 /\ c >= d + 1 ] (1, 3) f0(a, b) -> f4(e', e) [ 99 >= 1 /\ e >= 1 /\ c >= d + 1 ] (1, 2) f0(a, b) -> f4(e, 99) [ 99 >= 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(e, b) [ b >= a + 1 /\ c >= d + 1 ] (?, 1) f4(a, b) -> f4(a, e) [ b >= a + 1 ] start location: f0 leaf cost: 1 Complexity upper bound ? Time: 1.085 sec (SMT: 0.960 sec)