MAYBE Initial complexity problem: 1: T: (1, 1) f0(a, b, c) -> f1(0, b, c) (?, 1) f1(a, b, c) -> f1(a, b - 1, d) [ b >= 1 /\ d >= 1 ] (?, 1) f1(a, b, c) -> f1(a, b - 2, d) [ b >= 1 /\ 0 >= d ] (?, 1) f1(a, b, c) -> f4(a, b, d) [ 0 >= b ] (?, 1) f4(a, b, c) -> f4(1, b, d) [ c >= 1 ] (?, 1) f4(a, b, c) -> f4(2, b, d) [ 0 >= c ] start location: f0 leaf cost: 0 A polynomial rank function with Pol(f0) = 1 Pol(f1) = 1 Pol(f4) = -1 orients all transitions weakly and the transition f1(a, b, c) -> f4(a, b, d) [ 0 >= b ] strictly and produces the following problem: 2: T: (1, 1) f0(a, b, c) -> f1(0, b, c) (?, 1) f1(a, b, c) -> f1(a, b - 1, d) [ b >= 1 /\ d >= 1 ] (?, 1) f1(a, b, c) -> f1(a, b - 2, d) [ b >= 1 /\ 0 >= d ] (1, 1) f1(a, b, c) -> f4(a, b, d) [ 0 >= b ] (?, 1) f4(a, b, c) -> f4(1, b, d) [ c >= 1 ] (?, 1) f4(a, b, c) -> f4(2, b, d) [ 0 >= c ] start location: f0 leaf cost: 0 A polynomial rank function with Pol(f0) = V_2 Pol(f1) = V_2 Pol(f4) = V_2 orients all transitions weakly and the transitions f1(a, b, c) -> f1(a, b - 1, d) [ b >= 1 /\ d >= 1 ] f1(a, b, c) -> f1(a, b - 2, d) [ b >= 1 /\ 0 >= d ] strictly and produces the following problem: 3: T: (1, 1) f0(a, b, c) -> f1(0, b, c) (b, 1) f1(a, b, c) -> f1(a, b - 1, d) [ b >= 1 /\ d >= 1 ] (b, 1) f1(a, b, c) -> f1(a, b - 2, d) [ b >= 1 /\ 0 >= d ] (1, 1) f1(a, b, c) -> f4(a, b, d) [ 0 >= b ] (?, 1) f4(a, b, c) -> f4(1, b, d) [ c >= 1 ] (?, 1) f4(a, b, c) -> f4(2, b, d) [ 0 >= c ] start location: f0 leaf cost: 0 Applied AI with 'oct' on problem 3 to obtain the following invariants: For symbol f1: -X_1 >= 0 /\ X_1 >= 0 For symbol f4: -X_2 >= 0 /\ X_1 - X_2 >= 0 /\ X_1 >= 0 This yielded the following problem: 4: T: (?, 1) f4(a, b, c) -> f4(2, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ 0 >= c ] (?, 1) f4(a, b, c) -> f4(1, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ c >= 1 ] (1, 1) f1(a, b, c) -> f4(a, b, d) [ -a >= 0 /\ a >= 0 /\ 0 >= b ] (b, 1) f1(a, b, c) -> f1(a, b - 2, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ 0 >= d ] (b, 1) f1(a, b, c) -> f1(a, b - 1, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ d >= 1 ] (1, 1) f0(a, b, c) -> f1(0, b, c) start location: f0 leaf cost: 0 By chaining the transition f1(a, b, c) -> f4(a, b, d) [ -a >= 0 /\ a >= 0 /\ 0 >= b ] with all transitions in problem 4, the following new transitions are obtained: f1(a, b, c) -> f4(1, b, d') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 ] f1(a, b, c) -> f4(2, b, d') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ 0 >= d ] We thus obtain the following problem: 5: T: (1, 2) f1(a, b, c) -> f4(1, b, d') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 ] (1, 2) f1(a, b, c) -> f4(2, b, d') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ 0 >= d ] (?, 1) f4(a, b, c) -> f4(2, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ 0 >= c ] (?, 1) f4(a, b, c) -> f4(1, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ c >= 1 ] (b, 1) f1(a, b, c) -> f1(a, b - 2, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ 0 >= d ] (b, 1) f1(a, b, c) -> f1(a, b - 1, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ d >= 1 ] (1, 1) f0(a, b, c) -> f1(0, b, c) start location: f0 leaf cost: 0 By chaining the transition f1(a, b, c) -> f4(1, b, d') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 ] with all transitions in problem 5, the following new transitions are obtained: f1(a, b, c) -> f4(1, b, d'') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 ] f1(a, b, c) -> f4(2, b, d'') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ 0 >= d' ] We thus obtain the following problem: 6: T: (1, 3) f1(a, b, c) -> f4(1, b, d'') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 ] (1, 3) f1(a, b, c) -> f4(2, b, d'') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ 0 >= d' ] (1, 2) f1(a, b, c) -> f4(2, b, d') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ 0 >= d ] (?, 1) f4(a, b, c) -> f4(2, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ 0 >= c ] (?, 1) f4(a, b, c) -> f4(1, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ c >= 1 ] (b, 1) f1(a, b, c) -> f1(a, b - 2, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ 0 >= d ] (b, 1) f1(a, b, c) -> f1(a, b - 1, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ d >= 1 ] (1, 1) f0(a, b, c) -> f1(0, b, c) start location: f0 leaf cost: 0 By chaining the transition f1(a, b, c) -> f4(1, b, d'') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 ] with all transitions in problem 6, the following new transitions are obtained: f1(a, b, c) -> f4(1, b, d''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 ] f1(a, b, c) -> f4(2, b, d''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ 0 >= d'' ] We thus obtain the following problem: 7: T: (1, 4) f1(a, b, c) -> f4(1, b, d''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 ] (1, 4) f1(a, b, c) -> f4(2, b, d''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ 0 >= d'' ] (1, 3) f1(a, b, c) -> f4(2, b, d'') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ 0 >= d' ] (1, 2) f1(a, b, c) -> f4(2, b, d') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ 0 >= d ] (?, 1) f4(a, b, c) -> f4(2, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ 0 >= c ] (?, 1) f4(a, b, c) -> f4(1, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ c >= 1 ] (b, 1) f1(a, b, c) -> f1(a, b - 2, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ 0 >= d ] (b, 1) f1(a, b, c) -> f1(a, b - 1, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ d >= 1 ] (1, 1) f0(a, b, c) -> f1(0, b, c) start location: f0 leaf cost: 0 By chaining the transition f1(a, b, c) -> f4(1, b, d''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 ] with all transitions in problem 7, the following new transitions are obtained: f1(a, b, c) -> f4(1, b, d'''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 ] f1(a, b, c) -> f4(2, b, d'''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ 0 >= d''' ] We thus obtain the following problem: 8: T: (1, 5) f1(a, b, c) -> f4(1, b, d'''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 ] (1, 5) f1(a, b, c) -> f4(2, b, d'''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ 0 >= d''' ] (1, 4) f1(a, b, c) -> f4(2, b, d''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ 0 >= d'' ] (1, 3) f1(a, b, c) -> f4(2, b, d'') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ 0 >= d' ] (1, 2) f1(a, b, c) -> f4(2, b, d') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ 0 >= d ] (?, 1) f4(a, b, c) -> f4(2, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ 0 >= c ] (?, 1) f4(a, b, c) -> f4(1, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ c >= 1 ] (b, 1) f1(a, b, c) -> f1(a, b - 2, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ 0 >= d ] (b, 1) f1(a, b, c) -> f1(a, b - 1, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ d >= 1 ] (1, 1) f0(a, b, c) -> f1(0, b, c) start location: f0 leaf cost: 0 By chaining the transition f1(a, b, c) -> f4(1, b, d'''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 ] with all transitions in problem 8, the following new transitions are obtained: f1(a, b, c) -> f4(1, b, d''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 ] f1(a, b, c) -> f4(2, b, d''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ 0 >= d'''' ] We thus obtain the following problem: 9: T: (1, 6) f1(a, b, c) -> f4(1, b, d''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 ] (1, 6) f1(a, b, c) -> f4(2, b, d''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ 0 >= d'''' ] (1, 5) f1(a, b, c) -> f4(2, b, d'''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ 0 >= d''' ] (1, 4) f1(a, b, c) -> f4(2, b, d''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ 0 >= d'' ] (1, 3) f1(a, b, c) -> f4(2, b, d'') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ 0 >= d' ] (1, 2) f1(a, b, c) -> f4(2, b, d') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ 0 >= d ] (?, 1) f4(a, b, c) -> f4(2, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ 0 >= c ] (?, 1) f4(a, b, c) -> f4(1, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ c >= 1 ] (b, 1) f1(a, b, c) -> f1(a, b - 2, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ 0 >= d ] (b, 1) f1(a, b, c) -> f1(a, b - 1, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ d >= 1 ] (1, 1) f0(a, b, c) -> f1(0, b, c) start location: f0 leaf cost: 0 By chaining the transition f1(a, b, c) -> f4(1, b, d''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 ] with all transitions in problem 9, the following new transitions are obtained: f1(a, b, c) -> f4(1, b, d'''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 ] f1(a, b, c) -> f4(2, b, d'''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ 0 >= d''''' ] We thus obtain the following problem: 10: T: (1, 7) f1(a, b, c) -> f4(1, b, d'''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 ] (1, 7) f1(a, b, c) -> f4(2, b, d'''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ 0 >= d''''' ] (1, 6) f1(a, b, c) -> f4(2, b, d''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ 0 >= d'''' ] (1, 5) f1(a, b, c) -> f4(2, b, d'''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ 0 >= d''' ] (1, 4) f1(a, b, c) -> f4(2, b, d''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ 0 >= d'' ] (1, 3) f1(a, b, c) -> f4(2, b, d'') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ 0 >= d' ] (1, 2) f1(a, b, c) -> f4(2, b, d') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ 0 >= d ] (?, 1) f4(a, b, c) -> f4(2, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ 0 >= c ] (?, 1) f4(a, b, c) -> f4(1, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ c >= 1 ] (b, 1) f1(a, b, c) -> f1(a, b - 2, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ 0 >= d ] (b, 1) f1(a, b, c) -> f1(a, b - 1, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ d >= 1 ] (1, 1) f0(a, b, c) -> f1(0, b, c) start location: f0 leaf cost: 0 By chaining the transition f1(a, b, c) -> f4(1, b, d'''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 ] with all transitions in problem 10, the following new transitions are obtained: f1(a, b, c) -> f4(1, b, d''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 ] f1(a, b, c) -> f4(2, b, d''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ 0 >= d'''''' ] We thus obtain the following problem: 11: T: (1, 8) f1(a, b, c) -> f4(1, b, d''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 ] (1, 8) f1(a, b, c) -> f4(2, b, d''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ 0 >= d'''''' ] (1, 7) f1(a, b, c) -> f4(2, b, d'''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ 0 >= d''''' ] (1, 6) f1(a, b, c) -> f4(2, b, d''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ 0 >= d'''' ] (1, 5) f1(a, b, c) -> f4(2, b, d'''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ 0 >= d''' ] (1, 4) f1(a, b, c) -> f4(2, b, d''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ 0 >= d'' ] (1, 3) f1(a, b, c) -> f4(2, b, d'') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ 0 >= d' ] (1, 2) f1(a, b, c) -> f4(2, b, d') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ 0 >= d ] (?, 1) f4(a, b, c) -> f4(2, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ 0 >= c ] (?, 1) f4(a, b, c) -> f4(1, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ c >= 1 ] (b, 1) f1(a, b, c) -> f1(a, b - 2, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ 0 >= d ] (b, 1) f1(a, b, c) -> f1(a, b - 1, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ d >= 1 ] (1, 1) f0(a, b, c) -> f1(0, b, c) start location: f0 leaf cost: 0 By chaining the transition f1(a, b, c) -> f4(1, b, d''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 ] with all transitions in problem 11, the following new transitions are obtained: f1(a, b, c) -> f4(1, b, d'''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 ] f1(a, b, c) -> f4(2, b, d'''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ 0 >= d''''''' ] We thus obtain the following problem: 12: T: (1, 9) f1(a, b, c) -> f4(1, b, d'''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 ] (1, 9) f1(a, b, c) -> f4(2, b, d'''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ 0 >= d''''''' ] (1, 8) f1(a, b, c) -> f4(2, b, d''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ 0 >= d'''''' ] (1, 7) f1(a, b, c) -> f4(2, b, d'''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ 0 >= d''''' ] (1, 6) f1(a, b, c) -> f4(2, b, d''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ 0 >= d'''' ] (1, 5) f1(a, b, c) -> f4(2, b, d'''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ 0 >= d''' ] (1, 4) f1(a, b, c) -> f4(2, b, d''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ 0 >= d'' ] (1, 3) f1(a, b, c) -> f4(2, b, d'') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ 0 >= d' ] (1, 2) f1(a, b, c) -> f4(2, b, d') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ 0 >= d ] (?, 1) f4(a, b, c) -> f4(2, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ 0 >= c ] (?, 1) f4(a, b, c) -> f4(1, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ c >= 1 ] (b, 1) f1(a, b, c) -> f1(a, b - 2, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ 0 >= d ] (b, 1) f1(a, b, c) -> f1(a, b - 1, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ d >= 1 ] (1, 1) f0(a, b, c) -> f1(0, b, c) start location: f0 leaf cost: 0 By chaining the transition f1(a, b, c) -> f4(1, b, d'''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 ] with all transitions in problem 12, the following new transitions are obtained: f1(a, b, c) -> f4(1, b, d''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 ] f1(a, b, c) -> f4(2, b, d''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ 0 >= d'''''''' ] We thus obtain the following problem: 13: T: (1, 10) f1(a, b, c) -> f4(1, b, d''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 ] (1, 10) f1(a, b, c) -> f4(2, b, d''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ 0 >= d'''''''' ] (1, 9) f1(a, b, c) -> f4(2, b, d'''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ 0 >= d''''''' ] (1, 8) f1(a, b, c) -> f4(2, b, d''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ 0 >= d'''''' ] (1, 7) f1(a, b, c) -> f4(2, b, d'''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ 0 >= d''''' ] (1, 6) f1(a, b, c) -> f4(2, b, d''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ 0 >= d'''' ] (1, 5) f1(a, b, c) -> f4(2, b, d'''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ 0 >= d''' ] (1, 4) f1(a, b, c) -> f4(2, b, d''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ 0 >= d'' ] (1, 3) f1(a, b, c) -> f4(2, b, d'') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ 0 >= d' ] (1, 2) f1(a, b, c) -> f4(2, b, d') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ 0 >= d ] (?, 1) f4(a, b, c) -> f4(2, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ 0 >= c ] (?, 1) f4(a, b, c) -> f4(1, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ c >= 1 ] (b, 1) f1(a, b, c) -> f1(a, b - 2, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ 0 >= d ] (b, 1) f1(a, b, c) -> f1(a, b - 1, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ d >= 1 ] (1, 1) f0(a, b, c) -> f1(0, b, c) start location: f0 leaf cost: 0 By chaining the transition f1(a, b, c) -> f4(1, b, d''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 ] with all transitions in problem 13, the following new transitions are obtained: f1(a, b, c) -> f4(1, b, d'''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 ] f1(a, b, c) -> f4(2, b, d'''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ 0 >= d''''''''' ] We thus obtain the following problem: 14: T: (1, 11) f1(a, b, c) -> f4(1, b, d'''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 ] (1, 11) f1(a, b, c) -> f4(2, b, d'''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ 0 >= d''''''''' ] (1, 10) f1(a, b, c) -> f4(2, b, d''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ 0 >= d'''''''' ] (1, 9) f1(a, b, c) -> f4(2, b, d'''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ 0 >= d''''''' ] (1, 8) f1(a, b, c) -> f4(2, b, d''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ 0 >= d'''''' ] (1, 7) f1(a, b, c) -> f4(2, b, d'''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ 0 >= d''''' ] (1, 6) f1(a, b, c) -> f4(2, b, d''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ 0 >= d'''' ] (1, 5) f1(a, b, c) -> f4(2, b, d'''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ 0 >= d''' ] (1, 4) f1(a, b, c) -> f4(2, b, d''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ 0 >= d'' ] (1, 3) f1(a, b, c) -> f4(2, b, d'') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ 0 >= d' ] (1, 2) f1(a, b, c) -> f4(2, b, d') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ 0 >= d ] (?, 1) f4(a, b, c) -> f4(2, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ 0 >= c ] (?, 1) f4(a, b, c) -> f4(1, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ c >= 1 ] (b, 1) f1(a, b, c) -> f1(a, b - 2, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ 0 >= d ] (b, 1) f1(a, b, c) -> f1(a, b - 1, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ d >= 1 ] (1, 1) f0(a, b, c) -> f1(0, b, c) start location: f0 leaf cost: 0 By chaining the transition f1(a, b, c) -> f4(1, b, d'''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 ] with all transitions in problem 14, the following new transitions are obtained: f1(a, b, c) -> f4(1, b, d''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 ] f1(a, b, c) -> f4(2, b, d''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ 0 >= d'''''''''' ] We thus obtain the following problem: 15: T: (1, 12) f1(a, b, c) -> f4(1, b, d''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 ] (1, 12) f1(a, b, c) -> f4(2, b, d''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ 0 >= d'''''''''' ] (1, 11) f1(a, b, c) -> f4(2, b, d'''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ 0 >= d''''''''' ] (1, 10) f1(a, b, c) -> f4(2, b, d''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ 0 >= d'''''''' ] (1, 9) f1(a, b, c) -> f4(2, b, d'''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ 0 >= d''''''' ] (1, 8) f1(a, b, c) -> f4(2, b, d''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ 0 >= d'''''' ] (1, 7) f1(a, b, c) -> f4(2, b, d'''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ 0 >= d''''' ] (1, 6) f1(a, b, c) -> f4(2, b, d''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ 0 >= d'''' ] (1, 5) f1(a, b, c) -> f4(2, b, d'''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ 0 >= d''' ] (1, 4) f1(a, b, c) -> f4(2, b, d''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ 0 >= d'' ] (1, 3) f1(a, b, c) -> f4(2, b, d'') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ 0 >= d' ] (1, 2) f1(a, b, c) -> f4(2, b, d') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ 0 >= d ] (?, 1) f4(a, b, c) -> f4(2, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ 0 >= c ] (?, 1) f4(a, b, c) -> f4(1, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ c >= 1 ] (b, 1) f1(a, b, c) -> f1(a, b - 2, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ 0 >= d ] (b, 1) f1(a, b, c) -> f1(a, b - 1, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ d >= 1 ] (1, 1) f0(a, b, c) -> f1(0, b, c) start location: f0 leaf cost: 0 By chaining the transition f1(a, b, c) -> f4(1, b, d''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 ] with all transitions in problem 15, the following new transitions are obtained: f1(a, b, c) -> f4(1, b, d'''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ d''''''''''' >= 1 ] f1(a, b, c) -> f4(2, b, d'''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ 0 >= d''''''''''' ] We thus obtain the following problem: 16: T: (1, 13) f1(a, b, c) -> f4(1, b, d'''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ d''''''''''' >= 1 ] (1, 13) f1(a, b, c) -> f4(2, b, d'''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ 0 >= d''''''''''' ] (1, 12) f1(a, b, c) -> f4(2, b, d''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ 0 >= d'''''''''' ] (1, 11) f1(a, b, c) -> f4(2, b, d'''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ 0 >= d''''''''' ] (1, 10) f1(a, b, c) -> f4(2, b, d''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ 0 >= d'''''''' ] (1, 9) f1(a, b, c) -> f4(2, b, d'''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ 0 >= d''''''' ] (1, 8) f1(a, b, c) -> f4(2, b, d''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ 0 >= d'''''' ] (1, 7) f1(a, b, c) -> f4(2, b, d'''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ 0 >= d''''' ] (1, 6) f1(a, b, c) -> f4(2, b, d''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ 0 >= d'''' ] (1, 5) f1(a, b, c) -> f4(2, b, d'''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ 0 >= d''' ] (1, 4) f1(a, b, c) -> f4(2, b, d''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ 0 >= d'' ] (1, 3) f1(a, b, c) -> f4(2, b, d'') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ 0 >= d' ] (1, 2) f1(a, b, c) -> f4(2, b, d') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ 0 >= d ] (?, 1) f4(a, b, c) -> f4(2, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ 0 >= c ] (?, 1) f4(a, b, c) -> f4(1, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ c >= 1 ] (b, 1) f1(a, b, c) -> f1(a, b - 2, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ 0 >= d ] (b, 1) f1(a, b, c) -> f1(a, b - 1, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ d >= 1 ] (1, 1) f0(a, b, c) -> f1(0, b, c) start location: f0 leaf cost: 0 By chaining the transition f1(a, b, c) -> f4(1, b, d'''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ d''''''''''' >= 1 ] with all transitions in problem 16, the following new transitions are obtained: f1(a, b, c) -> f4(1, b, d''''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ d''''''''''' >= 1 /\ d'''''''''''' >= 1 ] f1(a, b, c) -> f4(2, b, d''''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ d''''''''''' >= 1 /\ 0 >= d'''''''''''' ] We thus obtain the following problem: 17: T: (1, 14) f1(a, b, c) -> f4(1, b, d''''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ d''''''''''' >= 1 /\ d'''''''''''' >= 1 ] (1, 14) f1(a, b, c) -> f4(2, b, d''''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ d''''''''''' >= 1 /\ 0 >= d'''''''''''' ] (1, 13) f1(a, b, c) -> f4(2, b, d'''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ 0 >= d''''''''''' ] (1, 12) f1(a, b, c) -> f4(2, b, d''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ 0 >= d'''''''''' ] (1, 11) f1(a, b, c) -> f4(2, b, d'''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ 0 >= d''''''''' ] (1, 10) f1(a, b, c) -> f4(2, b, d''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ 0 >= d'''''''' ] (1, 9) f1(a, b, c) -> f4(2, b, d'''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ 0 >= d''''''' ] (1, 8) f1(a, b, c) -> f4(2, b, d''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ 0 >= d'''''' ] (1, 7) f1(a, b, c) -> f4(2, b, d'''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ 0 >= d''''' ] (1, 6) f1(a, b, c) -> f4(2, b, d''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ 0 >= d'''' ] (1, 5) f1(a, b, c) -> f4(2, b, d'''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ 0 >= d''' ] (1, 4) f1(a, b, c) -> f4(2, b, d''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ 0 >= d'' ] (1, 3) f1(a, b, c) -> f4(2, b, d'') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ 0 >= d' ] (1, 2) f1(a, b, c) -> f4(2, b, d') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ 0 >= d ] (?, 1) f4(a, b, c) -> f4(2, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ 0 >= c ] (?, 1) f4(a, b, c) -> f4(1, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ c >= 1 ] (b, 1) f1(a, b, c) -> f1(a, b - 2, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ 0 >= d ] (b, 1) f1(a, b, c) -> f1(a, b - 1, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ d >= 1 ] (1, 1) f0(a, b, c) -> f1(0, b, c) start location: f0 leaf cost: 0 By chaining the transition f1(a, b, c) -> f4(1, b, d''''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ d''''''''''' >= 1 /\ d'''''''''''' >= 1 ] with all transitions in problem 17, the following new transitions are obtained: f1(a, b, c) -> f4(1, b, d'''''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ d''''''''''' >= 1 /\ d'''''''''''' >= 1 /\ d''''''''''''' >= 1 ] f1(a, b, c) -> f4(2, b, d'''''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ d''''''''''' >= 1 /\ d'''''''''''' >= 1 /\ 0 >= d''''''''''''' ] We thus obtain the following problem: 18: T: (1, 15) f1(a, b, c) -> f4(1, b, d'''''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ d''''''''''' >= 1 /\ d'''''''''''' >= 1 /\ d''''''''''''' >= 1 ] (1, 15) f1(a, b, c) -> f4(2, b, d'''''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ d''''''''''' >= 1 /\ d'''''''''''' >= 1 /\ 0 >= d''''''''''''' ] (1, 14) f1(a, b, c) -> f4(2, b, d''''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ d''''''''''' >= 1 /\ 0 >= d'''''''''''' ] (1, 13) f1(a, b, c) -> f4(2, b, d'''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ 0 >= d''''''''''' ] (1, 12) f1(a, b, c) -> f4(2, b, d''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ 0 >= d'''''''''' ] (1, 11) f1(a, b, c) -> f4(2, b, d'''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ 0 >= d''''''''' ] (1, 10) f1(a, b, c) -> f4(2, b, d''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ 0 >= d'''''''' ] (1, 9) f1(a, b, c) -> f4(2, b, d'''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ 0 >= d''''''' ] (1, 8) f1(a, b, c) -> f4(2, b, d''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ 0 >= d'''''' ] (1, 7) f1(a, b, c) -> f4(2, b, d'''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ 0 >= d''''' ] (1, 6) f1(a, b, c) -> f4(2, b, d''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ 0 >= d'''' ] (1, 5) f1(a, b, c) -> f4(2, b, d'''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ 0 >= d''' ] (1, 4) f1(a, b, c) -> f4(2, b, d''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ 0 >= d'' ] (1, 3) f1(a, b, c) -> f4(2, b, d'') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ 0 >= d' ] (1, 2) f1(a, b, c) -> f4(2, b, d') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ 0 >= d ] (?, 1) f4(a, b, c) -> f4(2, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ 0 >= c ] (?, 1) f4(a, b, c) -> f4(1, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ c >= 1 ] (b, 1) f1(a, b, c) -> f1(a, b - 2, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ 0 >= d ] (b, 1) f1(a, b, c) -> f1(a, b - 1, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ d >= 1 ] (1, 1) f0(a, b, c) -> f1(0, b, c) start location: f0 leaf cost: 0 By chaining the transition f1(a, b, c) -> f4(1, b, d'''''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ d''''''''''' >= 1 /\ d'''''''''''' >= 1 /\ d''''''''''''' >= 1 ] with all transitions in problem 18, the following new transitions are obtained: f1(a, b, c) -> f4(1, b, d''''''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ d''''''''''' >= 1 /\ d'''''''''''' >= 1 /\ d''''''''''''' >= 1 /\ d'''''''''''''' >= 1 ] f1(a, b, c) -> f4(2, b, d''''''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ d''''''''''' >= 1 /\ d'''''''''''' >= 1 /\ d''''''''''''' >= 1 /\ 0 >= d'''''''''''''' ] We thus obtain the following problem: 19: T: (1, 16) f1(a, b, c) -> f4(1, b, d''''''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ d''''''''''' >= 1 /\ d'''''''''''' >= 1 /\ d''''''''''''' >= 1 /\ d'''''''''''''' >= 1 ] (1, 16) f1(a, b, c) -> f4(2, b, d''''''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ d''''''''''' >= 1 /\ d'''''''''''' >= 1 /\ d''''''''''''' >= 1 /\ 0 >= d'''''''''''''' ] (1, 15) f1(a, b, c) -> f4(2, b, d'''''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ d''''''''''' >= 1 /\ d'''''''''''' >= 1 /\ 0 >= d''''''''''''' ] (1, 14) f1(a, b, c) -> f4(2, b, d''''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ d''''''''''' >= 1 /\ 0 >= d'''''''''''' ] (1, 13) f1(a, b, c) -> f4(2, b, d'''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ d'''''''''' >= 1 /\ 0 >= d''''''''''' ] (1, 12) f1(a, b, c) -> f4(2, b, d''''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ d''''''''' >= 1 /\ 0 >= d'''''''''' ] (1, 11) f1(a, b, c) -> f4(2, b, d'''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ d'''''''' >= 1 /\ 0 >= d''''''''' ] (1, 10) f1(a, b, c) -> f4(2, b, d''''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ d''''''' >= 1 /\ 0 >= d'''''''' ] (1, 9) f1(a, b, c) -> f4(2, b, d'''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ d'''''' >= 1 /\ 0 >= d''''''' ] (1, 8) f1(a, b, c) -> f4(2, b, d''''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ d''''' >= 1 /\ 0 >= d'''''' ] (1, 7) f1(a, b, c) -> f4(2, b, d'''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ d'''' >= 1 /\ 0 >= d''''' ] (1, 6) f1(a, b, c) -> f4(2, b, d''''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ d''' >= 1 /\ 0 >= d'''' ] (1, 5) f1(a, b, c) -> f4(2, b, d'''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ d'' >= 1 /\ 0 >= d''' ] (1, 4) f1(a, b, c) -> f4(2, b, d''') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ d' >= 1 /\ 0 >= d'' ] (1, 3) f1(a, b, c) -> f4(2, b, d'') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ d >= 1 /\ -b + 1 >= 0 /\ 1 >= 0 /\ 0 >= d' ] (1, 2) f1(a, b, c) -> f4(2, b, d') [ -a >= 0 /\ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a - b >= 0 /\ 0 >= d ] (?, 1) f4(a, b, c) -> f4(2, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ 0 >= c ] (?, 1) f4(a, b, c) -> f4(1, b, d) [ -b >= 0 /\ a - b >= 0 /\ a >= 0 /\ c >= 1 ] (b, 1) f1(a, b, c) -> f1(a, b - 2, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ 0 >= d ] (b, 1) f1(a, b, c) -> f1(a, b - 1, d) [ -a >= 0 /\ a >= 0 /\ b >= 1 /\ d >= 1 ] (1, 1) f0(a, b, c) -> f1(0, b, c) start location: f0 leaf cost: 0 Complexity upper bound ? Time: 2.388 sec (SMT: 2.123 sec)