MAYBE Initial complexity problem: 1: T: (1, 1) f3(a, b) -> f0(2, b) (?, 1) f0(a, b) -> f0(a + 1, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a - 1, c) [ 0 >= c ] start location: f3 leaf cost: 0 By chaining the transition f3(a, b) -> f0(2, b) with all transitions in problem 1, the following new transitions are obtained: f3(a, b) -> f0(1, c) [ 0 >= c ] f3(a, b) -> f0(3, c) [ c >= 1 ] We thus obtain the following problem: 2: T: (1, 2) f3(a, b) -> f0(1, c) [ 0 >= c ] (1, 2) f3(a, b) -> f0(3, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a + 1, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a - 1, c) [ 0 >= c ] start location: f3 leaf cost: 0 By chaining the transition f3(a, b) -> f0(1, c) [ 0 >= c ] with all transitions in problem 2, the following new transitions are obtained: f3(a, b) -> f0(0, c') [ 0 >= c /\ 0 >= c' ] f3(a, b) -> f0(2, c') [ 0 >= c /\ c' >= 1 ] We thus obtain the following problem: 3: T: (1, 3) f3(a, b) -> f0(0, c') [ 0 >= c /\ 0 >= c' ] (1, 3) f3(a, b) -> f0(2, c') [ 0 >= c /\ c' >= 1 ] (1, 2) f3(a, b) -> f0(3, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a + 1, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a - 1, c) [ 0 >= c ] start location: f3 leaf cost: 0 By chaining the transition f3(a, b) -> f0(0, c') [ 0 >= c /\ 0 >= c' ] with all transitions in problem 3, the following new transitions are obtained: f3(a, b) -> f0(-1, c'') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' ] f3(a, b) -> f0(1, c'') [ 0 >= c /\ 0 >= c' /\ c'' >= 1 ] We thus obtain the following problem: 4: T: (1, 4) f3(a, b) -> f0(-1, c'') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' ] (1, 4) f3(a, b) -> f0(1, c'') [ 0 >= c /\ 0 >= c' /\ c'' >= 1 ] (1, 3) f3(a, b) -> f0(2, c') [ 0 >= c /\ c' >= 1 ] (1, 2) f3(a, b) -> f0(3, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a + 1, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a - 1, c) [ 0 >= c ] start location: f3 leaf cost: 0 By chaining the transition f3(a, b) -> f0(-1, c'') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' ] with all transitions in problem 4, the following new transitions are obtained: f3(a, b) -> f0(-2, c''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' ] f3(a, b) -> f0(0, c''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ c''' >= 1 ] We thus obtain the following problem: 5: T: (1, 5) f3(a, b) -> f0(-2, c''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' ] (1, 5) f3(a, b) -> f0(0, c''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ c''' >= 1 ] (1, 4) f3(a, b) -> f0(1, c'') [ 0 >= c /\ 0 >= c' /\ c'' >= 1 ] (1, 3) f3(a, b) -> f0(2, c') [ 0 >= c /\ c' >= 1 ] (1, 2) f3(a, b) -> f0(3, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a + 1, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a - 1, c) [ 0 >= c ] start location: f3 leaf cost: 0 By chaining the transition f3(a, b) -> f0(-2, c''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' ] with all transitions in problem 5, the following new transitions are obtained: f3(a, b) -> f0(-3, c'''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' ] f3(a, b) -> f0(-1, c'''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ c'''' >= 1 ] We thus obtain the following problem: 6: T: (1, 6) f3(a, b) -> f0(-3, c'''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' ] (1, 6) f3(a, b) -> f0(-1, c'''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ c'''' >= 1 ] (1, 5) f3(a, b) -> f0(0, c''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ c''' >= 1 ] (1, 4) f3(a, b) -> f0(1, c'') [ 0 >= c /\ 0 >= c' /\ c'' >= 1 ] (1, 3) f3(a, b) -> f0(2, c') [ 0 >= c /\ c' >= 1 ] (1, 2) f3(a, b) -> f0(3, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a + 1, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a - 1, c) [ 0 >= c ] start location: f3 leaf cost: 0 By chaining the transition f3(a, b) -> f0(-3, c'''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' ] with all transitions in problem 6, the following new transitions are obtained: f3(a, b) -> f0(-4, c''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' ] f3(a, b) -> f0(-2, c''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ c''''' >= 1 ] We thus obtain the following problem: 7: T: (1, 7) f3(a, b) -> f0(-4, c''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' ] (1, 7) f3(a, b) -> f0(-2, c''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ c''''' >= 1 ] (1, 6) f3(a, b) -> f0(-1, c'''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ c'''' >= 1 ] (1, 5) f3(a, b) -> f0(0, c''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ c''' >= 1 ] (1, 4) f3(a, b) -> f0(1, c'') [ 0 >= c /\ 0 >= c' /\ c'' >= 1 ] (1, 3) f3(a, b) -> f0(2, c') [ 0 >= c /\ c' >= 1 ] (1, 2) f3(a, b) -> f0(3, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a + 1, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a - 1, c) [ 0 >= c ] start location: f3 leaf cost: 0 By chaining the transition f3(a, b) -> f0(-4, c''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' ] with all transitions in problem 7, the following new transitions are obtained: f3(a, b) -> f0(-5, c'''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' ] f3(a, b) -> f0(-3, c'''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ c'''''' >= 1 ] We thus obtain the following problem: 8: T: (1, 8) f3(a, b) -> f0(-5, c'''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' ] (1, 8) f3(a, b) -> f0(-3, c'''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ c'''''' >= 1 ] (1, 7) f3(a, b) -> f0(-2, c''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ c''''' >= 1 ] (1, 6) f3(a, b) -> f0(-1, c'''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ c'''' >= 1 ] (1, 5) f3(a, b) -> f0(0, c''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ c''' >= 1 ] (1, 4) f3(a, b) -> f0(1, c'') [ 0 >= c /\ 0 >= c' /\ c'' >= 1 ] (1, 3) f3(a, b) -> f0(2, c') [ 0 >= c /\ c' >= 1 ] (1, 2) f3(a, b) -> f0(3, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a + 1, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a - 1, c) [ 0 >= c ] start location: f3 leaf cost: 0 By chaining the transition f3(a, b) -> f0(-5, c'''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' ] with all transitions in problem 8, the following new transitions are obtained: f3(a, b) -> f0(-6, c''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' ] f3(a, b) -> f0(-4, c''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ c''''''' >= 1 ] We thus obtain the following problem: 9: T: (1, 9) f3(a, b) -> f0(-6, c''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' ] (1, 9) f3(a, b) -> f0(-4, c''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ c''''''' >= 1 ] (1, 8) f3(a, b) -> f0(-3, c'''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ c'''''' >= 1 ] (1, 7) f3(a, b) -> f0(-2, c''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ c''''' >= 1 ] (1, 6) f3(a, b) -> f0(-1, c'''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ c'''' >= 1 ] (1, 5) f3(a, b) -> f0(0, c''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ c''' >= 1 ] (1, 4) f3(a, b) -> f0(1, c'') [ 0 >= c /\ 0 >= c' /\ c'' >= 1 ] (1, 3) f3(a, b) -> f0(2, c') [ 0 >= c /\ c' >= 1 ] (1, 2) f3(a, b) -> f0(3, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a + 1, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a - 1, c) [ 0 >= c ] start location: f3 leaf cost: 0 By chaining the transition f3(a, b) -> f0(-6, c''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' ] with all transitions in problem 9, the following new transitions are obtained: f3(a, b) -> f0(-7, c'''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' ] f3(a, b) -> f0(-5, c'''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ c'''''''' >= 1 ] We thus obtain the following problem: 10: T: (1, 10) f3(a, b) -> f0(-7, c'''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' ] (1, 10) f3(a, b) -> f0(-5, c'''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ c'''''''' >= 1 ] (1, 9) f3(a, b) -> f0(-4, c''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ c''''''' >= 1 ] (1, 8) f3(a, b) -> f0(-3, c'''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ c'''''' >= 1 ] (1, 7) f3(a, b) -> f0(-2, c''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ c''''' >= 1 ] (1, 6) f3(a, b) -> f0(-1, c'''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ c'''' >= 1 ] (1, 5) f3(a, b) -> f0(0, c''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ c''' >= 1 ] (1, 4) f3(a, b) -> f0(1, c'') [ 0 >= c /\ 0 >= c' /\ c'' >= 1 ] (1, 3) f3(a, b) -> f0(2, c') [ 0 >= c /\ c' >= 1 ] (1, 2) f3(a, b) -> f0(3, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a + 1, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a - 1, c) [ 0 >= c ] start location: f3 leaf cost: 0 By chaining the transition f3(a, b) -> f0(-7, c'''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' ] with all transitions in problem 10, the following new transitions are obtained: f3(a, b) -> f0(-8, c''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' ] f3(a, b) -> f0(-6, c''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ c''''''''' >= 1 ] We thus obtain the following problem: 11: T: (1, 11) f3(a, b) -> f0(-8, c''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' ] (1, 11) f3(a, b) -> f0(-6, c''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ c''''''''' >= 1 ] (1, 10) f3(a, b) -> f0(-5, c'''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ c'''''''' >= 1 ] (1, 9) f3(a, b) -> f0(-4, c''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ c''''''' >= 1 ] (1, 8) f3(a, b) -> f0(-3, c'''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ c'''''' >= 1 ] (1, 7) f3(a, b) -> f0(-2, c''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ c''''' >= 1 ] (1, 6) f3(a, b) -> f0(-1, c'''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ c'''' >= 1 ] (1, 5) f3(a, b) -> f0(0, c''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ c''' >= 1 ] (1, 4) f3(a, b) -> f0(1, c'') [ 0 >= c /\ 0 >= c' /\ c'' >= 1 ] (1, 3) f3(a, b) -> f0(2, c') [ 0 >= c /\ c' >= 1 ] (1, 2) f3(a, b) -> f0(3, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a + 1, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a - 1, c) [ 0 >= c ] start location: f3 leaf cost: 0 By chaining the transition f3(a, b) -> f0(-8, c''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' ] with all transitions in problem 11, the following new transitions are obtained: f3(a, b) -> f0(-9, c'''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' ] f3(a, b) -> f0(-7, c'''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ c'''''''''' >= 1 ] We thus obtain the following problem: 12: T: (1, 12) f3(a, b) -> f0(-9, c'''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' ] (1, 12) f3(a, b) -> f0(-7, c'''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ c'''''''''' >= 1 ] (1, 11) f3(a, b) -> f0(-6, c''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ c''''''''' >= 1 ] (1, 10) f3(a, b) -> f0(-5, c'''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ c'''''''' >= 1 ] (1, 9) f3(a, b) -> f0(-4, c''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ c''''''' >= 1 ] (1, 8) f3(a, b) -> f0(-3, c'''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ c'''''' >= 1 ] (1, 7) f3(a, b) -> f0(-2, c''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ c''''' >= 1 ] (1, 6) f3(a, b) -> f0(-1, c'''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ c'''' >= 1 ] (1, 5) f3(a, b) -> f0(0, c''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ c''' >= 1 ] (1, 4) f3(a, b) -> f0(1, c'') [ 0 >= c /\ 0 >= c' /\ c'' >= 1 ] (1, 3) f3(a, b) -> f0(2, c') [ 0 >= c /\ c' >= 1 ] (1, 2) f3(a, b) -> f0(3, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a + 1, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a - 1, c) [ 0 >= c ] start location: f3 leaf cost: 0 By chaining the transition f3(a, b) -> f0(-9, c'''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' ] with all transitions in problem 12, the following new transitions are obtained: f3(a, b) -> f0(-10, c''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ 0 >= c''''''''''' ] f3(a, b) -> f0(-8, c''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ c''''''''''' >= 1 ] We thus obtain the following problem: 13: T: (1, 13) f3(a, b) -> f0(-10, c''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ 0 >= c''''''''''' ] (1, 13) f3(a, b) -> f0(-8, c''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ c''''''''''' >= 1 ] (1, 12) f3(a, b) -> f0(-7, c'''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ c'''''''''' >= 1 ] (1, 11) f3(a, b) -> f0(-6, c''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ c''''''''' >= 1 ] (1, 10) f3(a, b) -> f0(-5, c'''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ c'''''''' >= 1 ] (1, 9) f3(a, b) -> f0(-4, c''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ c''''''' >= 1 ] (1, 8) f3(a, b) -> f0(-3, c'''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ c'''''' >= 1 ] (1, 7) f3(a, b) -> f0(-2, c''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ c''''' >= 1 ] (1, 6) f3(a, b) -> f0(-1, c'''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ c'''' >= 1 ] (1, 5) f3(a, b) -> f0(0, c''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ c''' >= 1 ] (1, 4) f3(a, b) -> f0(1, c'') [ 0 >= c /\ 0 >= c' /\ c'' >= 1 ] (1, 3) f3(a, b) -> f0(2, c') [ 0 >= c /\ c' >= 1 ] (1, 2) f3(a, b) -> f0(3, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a + 1, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a - 1, c) [ 0 >= c ] start location: f3 leaf cost: 0 By chaining the transition f3(a, b) -> f0(-10, c''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ 0 >= c''''''''''' ] with all transitions in problem 13, the following new transitions are obtained: f3(a, b) -> f0(-11, c'''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ 0 >= c''''''''''' /\ 0 >= c'''''''''''' ] f3(a, b) -> f0(-9, c'''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ 0 >= c''''''''''' /\ c'''''''''''' >= 1 ] We thus obtain the following problem: 14: T: (1, 14) f3(a, b) -> f0(-11, c'''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ 0 >= c''''''''''' /\ 0 >= c'''''''''''' ] (1, 14) f3(a, b) -> f0(-9, c'''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ 0 >= c''''''''''' /\ c'''''''''''' >= 1 ] (1, 13) f3(a, b) -> f0(-8, c''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ c''''''''''' >= 1 ] (1, 12) f3(a, b) -> f0(-7, c'''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ c'''''''''' >= 1 ] (1, 11) f3(a, b) -> f0(-6, c''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ c''''''''' >= 1 ] (1, 10) f3(a, b) -> f0(-5, c'''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ c'''''''' >= 1 ] (1, 9) f3(a, b) -> f0(-4, c''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ c''''''' >= 1 ] (1, 8) f3(a, b) -> f0(-3, c'''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ c'''''' >= 1 ] (1, 7) f3(a, b) -> f0(-2, c''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ c''''' >= 1 ] (1, 6) f3(a, b) -> f0(-1, c'''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ c'''' >= 1 ] (1, 5) f3(a, b) -> f0(0, c''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ c''' >= 1 ] (1, 4) f3(a, b) -> f0(1, c'') [ 0 >= c /\ 0 >= c' /\ c'' >= 1 ] (1, 3) f3(a, b) -> f0(2, c') [ 0 >= c /\ c' >= 1 ] (1, 2) f3(a, b) -> f0(3, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a + 1, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a - 1, c) [ 0 >= c ] start location: f3 leaf cost: 0 By chaining the transition f3(a, b) -> f0(-11, c'''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ 0 >= c''''''''''' /\ 0 >= c'''''''''''' ] with all transitions in problem 14, the following new transitions are obtained: f3(a, b) -> f0(-12, c''''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ 0 >= c''''''''''' /\ 0 >= c'''''''''''' /\ 0 >= c''''''''''''' ] f3(a, b) -> f0(-10, c''''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ 0 >= c''''''''''' /\ 0 >= c'''''''''''' /\ c''''''''''''' >= 1 ] We thus obtain the following problem: 15: T: (1, 15) f3(a, b) -> f0(-12, c''''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ 0 >= c''''''''''' /\ 0 >= c'''''''''''' /\ 0 >= c''''''''''''' ] (1, 15) f3(a, b) -> f0(-10, c''''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ 0 >= c''''''''''' /\ 0 >= c'''''''''''' /\ c''''''''''''' >= 1 ] (1, 14) f3(a, b) -> f0(-9, c'''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ 0 >= c''''''''''' /\ c'''''''''''' >= 1 ] (1, 13) f3(a, b) -> f0(-8, c''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ c''''''''''' >= 1 ] (1, 12) f3(a, b) -> f0(-7, c'''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ c'''''''''' >= 1 ] (1, 11) f3(a, b) -> f0(-6, c''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ c''''''''' >= 1 ] (1, 10) f3(a, b) -> f0(-5, c'''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ c'''''''' >= 1 ] (1, 9) f3(a, b) -> f0(-4, c''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ c''''''' >= 1 ] (1, 8) f3(a, b) -> f0(-3, c'''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ c'''''' >= 1 ] (1, 7) f3(a, b) -> f0(-2, c''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ c''''' >= 1 ] (1, 6) f3(a, b) -> f0(-1, c'''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ c'''' >= 1 ] (1, 5) f3(a, b) -> f0(0, c''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ c''' >= 1 ] (1, 4) f3(a, b) -> f0(1, c'') [ 0 >= c /\ 0 >= c' /\ c'' >= 1 ] (1, 3) f3(a, b) -> f0(2, c') [ 0 >= c /\ c' >= 1 ] (1, 2) f3(a, b) -> f0(3, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a + 1, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a - 1, c) [ 0 >= c ] start location: f3 leaf cost: 0 By chaining the transition f3(a, b) -> f0(-12, c''''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ 0 >= c''''''''''' /\ 0 >= c'''''''''''' /\ 0 >= c''''''''''''' ] with all transitions in problem 15, the following new transitions are obtained: f3(a, b) -> f0(-13, c'''''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ 0 >= c''''''''''' /\ 0 >= c'''''''''''' /\ 0 >= c''''''''''''' /\ 0 >= c'''''''''''''' ] f3(a, b) -> f0(-11, c'''''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ 0 >= c''''''''''' /\ 0 >= c'''''''''''' /\ 0 >= c''''''''''''' /\ c'''''''''''''' >= 1 ] We thus obtain the following problem: 16: T: (1, 16) f3(a, b) -> f0(-13, c'''''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ 0 >= c''''''''''' /\ 0 >= c'''''''''''' /\ 0 >= c''''''''''''' /\ 0 >= c'''''''''''''' ] (1, 16) f3(a, b) -> f0(-11, c'''''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ 0 >= c''''''''''' /\ 0 >= c'''''''''''' /\ 0 >= c''''''''''''' /\ c'''''''''''''' >= 1 ] (1, 15) f3(a, b) -> f0(-10, c''''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ 0 >= c''''''''''' /\ 0 >= c'''''''''''' /\ c''''''''''''' >= 1 ] (1, 14) f3(a, b) -> f0(-9, c'''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ 0 >= c''''''''''' /\ c'''''''''''' >= 1 ] (1, 13) f3(a, b) -> f0(-8, c''''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ 0 >= c'''''''''' /\ c''''''''''' >= 1 ] (1, 12) f3(a, b) -> f0(-7, c'''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ 0 >= c''''''''' /\ c'''''''''' >= 1 ] (1, 11) f3(a, b) -> f0(-6, c''''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ 0 >= c'''''''' /\ c''''''''' >= 1 ] (1, 10) f3(a, b) -> f0(-5, c'''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ 0 >= c''''''' /\ c'''''''' >= 1 ] (1, 9) f3(a, b) -> f0(-4, c''''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ 0 >= c'''''' /\ c''''''' >= 1 ] (1, 8) f3(a, b) -> f0(-3, c'''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ 0 >= c''''' /\ c'''''' >= 1 ] (1, 7) f3(a, b) -> f0(-2, c''''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ 0 >= c'''' /\ c''''' >= 1 ] (1, 6) f3(a, b) -> f0(-1, c'''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ 0 >= c''' /\ c'''' >= 1 ] (1, 5) f3(a, b) -> f0(0, c''') [ 0 >= c /\ 0 >= c' /\ 0 >= c'' /\ c''' >= 1 ] (1, 4) f3(a, b) -> f0(1, c'') [ 0 >= c /\ 0 >= c' /\ c'' >= 1 ] (1, 3) f3(a, b) -> f0(2, c') [ 0 >= c /\ c' >= 1 ] (1, 2) f3(a, b) -> f0(3, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a + 1, c) [ c >= 1 ] (?, 1) f0(a, b) -> f0(a - 1, c) [ 0 >= c ] start location: f3 leaf cost: 0 Complexity upper bound ? Time: 1.127 sec (SMT: 1.014 sec)