MAYBE Initial complexity problem: 1: T: (1, 1) f0(a, b, c, d) -> f6(e, 0, c, d) (?, 1) f6(a, b, c, d) -> f10(a - 1, b + 1, c, d) [ a >= 1 ] (?, 1) f10(a, b, c, d) -> f14(a, b - 1, a - 1, d) [ b >= 1 ] (?, 1) f14(a, b, c, d) -> f14(a, b, c - 1, 0) [ c >= 1 ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ c >= 1 /\ 0 >= e + 1 ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ c >= 1 /\ e >= 1 ] (?, 1) f14(a, b, c, d) -> f10(a, b, c, d) [ 0 >= c ] (?, 1) f10(a, b, c, d) -> f6(a, b, c, d) [ 0 >= b ] (?, 1) f6(a, b, c, d) -> f25(a, b, c, d) [ 0 >= a ] 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, c, d) -> f6(e, 0, c, d) (?, 1) f6(a, b, c, d) -> f10(a - 1, b + 1, c, d) [ a >= 1 ] (?, 1) f10(a, b, c, d) -> f14(a, b - 1, a - 1, d) [ b >= 1 ] (?, 1) f14(a, b, c, d) -> f14(a, b, c - 1, 0) [ c >= 1 ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ c >= 1 /\ 0 >= e + 1 ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ c >= 1 /\ e >= 1 ] (?, 1) f14(a, b, c, d) -> f10(a, b, c, d) [ 0 >= c ] (?, 1) f10(a, b, c, d) -> f6(a, b, c, d) [ 0 >= b ] start location: f0 leaf cost: 1 Applied AI with 'oct' on problem 2 to obtain the following invariants: For symbol f10: X_1 >= 0 For symbol f14: X_1 - X_3 - 1 >= 0 /\ X_3 + 1 >= 0 /\ X_2 + X_3 + 1 >= 0 /\ X_1 + X_3 + 1 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 >= 0 /\ X_1 >= 0 For symbol f6: -X_2 >= 0 This yielded the following problem: 3: T: (?, 1) f10(a, b, c, d) -> f6(a, b, c, d) [ a >= 0 /\ 0 >= b ] (?, 1) f14(a, b, c, d) -> f10(a, b, c, d) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= c ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 /\ e >= 1 ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 /\ 0 >= e + 1 ] (?, 1) f14(a, b, c, d) -> f14(a, b, c - 1, 0) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 ] (?, 1) f10(a, b, c, d) -> f14(a, b - 1, a - 1, d) [ a >= 0 /\ b >= 1 ] (?, 1) f6(a, b, c, d) -> f10(a - 1, b + 1, c, d) [ -b >= 0 /\ a >= 1 ] (1, 1) f0(a, b, c, d) -> f6(e, 0, c, d) start location: f0 leaf cost: 1 By chaining the transition f10(a, b, c, d) -> f6(a, b, c, d) [ a >= 0 /\ 0 >= b ] with all transitions in problem 3, the following new transition is obtained: f10(a, b, c, d) -> f10(a - 1, b + 1, c, d) [ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a >= 1 ] We thus obtain the following problem: 4: T: (?, 2) f10(a, b, c, d) -> f10(a - 1, b + 1, c, d) [ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a >= 1 ] (?, 1) f14(a, b, c, d) -> f10(a, b, c, d) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= c ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 /\ e >= 1 ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 /\ 0 >= e + 1 ] (?, 1) f14(a, b, c, d) -> f14(a, b, c - 1, 0) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 ] (?, 1) f10(a, b, c, d) -> f14(a, b - 1, a - 1, d) [ a >= 0 /\ b >= 1 ] (?, 1) f6(a, b, c, d) -> f10(a - 1, b + 1, c, d) [ -b >= 0 /\ a >= 1 ] (1, 1) f0(a, b, c, d) -> f6(e, 0, c, d) start location: f0 leaf cost: 1 Repeatedly propagating knowledge in problem 4 produces the following problem: 5: T: (?, 2) f10(a, b, c, d) -> f10(a - 1, b + 1, c, d) [ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a >= 1 ] (?, 1) f14(a, b, c, d) -> f10(a, b, c, d) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= c ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 /\ e >= 1 ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 /\ 0 >= e + 1 ] (?, 1) f14(a, b, c, d) -> f14(a, b, c - 1, 0) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 ] (?, 1) f10(a, b, c, d) -> f14(a, b - 1, a - 1, d) [ a >= 0 /\ b >= 1 ] (1, 1) f6(a, b, c, d) -> f10(a - 1, b + 1, c, d) [ -b >= 0 /\ a >= 1 ] (1, 1) f0(a, b, c, d) -> f6(e, 0, c, d) start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c, d) -> f6(e, 0, c, d) with all transitions in problem 5, the following new transition is obtained: f0(a, b, c, d) -> f10(e - 1, 1, c, d) [ 0 >= 0 /\ e >= 1 ] We thus obtain the following problem: 6: T: (1, 2) f0(a, b, c, d) -> f10(e - 1, 1, c, d) [ 0 >= 0 /\ e >= 1 ] (?, 2) f10(a, b, c, d) -> f10(a - 1, b + 1, c, d) [ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a >= 1 ] (?, 1) f14(a, b, c, d) -> f10(a, b, c, d) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= c ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 /\ e >= 1 ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 /\ 0 >= e + 1 ] (?, 1) f14(a, b, c, d) -> f14(a, b, c - 1, 0) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 ] (?, 1) f10(a, b, c, d) -> f14(a, b - 1, a - 1, d) [ a >= 0 /\ b >= 1 ] (1, 1) f6(a, b, c, d) -> f10(a - 1, b + 1, c, d) [ -b >= 0 /\ a >= 1 ] start location: f0 leaf cost: 1 Testing for reachability in the complexity graph removes the following transition from problem 6: f6(a, b, c, d) -> f10(a - 1, b + 1, c, d) [ -b >= 0 /\ a >= 1 ] We thus obtain the following problem: 7: T: (?, 2) f10(a, b, c, d) -> f10(a - 1, b + 1, c, d) [ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a >= 1 ] (?, 1) f14(a, b, c, d) -> f14(a, b, c - 1, 0) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 /\ 0 >= e + 1 ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 /\ e >= 1 ] (?, 1) f14(a, b, c, d) -> f10(a, b, c, d) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= c ] (?, 1) f10(a, b, c, d) -> f14(a, b - 1, a - 1, d) [ a >= 0 /\ b >= 1 ] (1, 2) f0(a, b, c, d) -> f10(e - 1, 1, c, d) [ 0 >= 0 /\ e >= 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c, d) -> f10(e - 1, 1, c, d) [ 0 >= 0 /\ e >= 1 ] with all transitions in problem 7, the following new transition is obtained: f0(a, b, c, d) -> f14(e - 1, 0, e - 2, d) [ 0 >= 0 /\ e >= 1 /\ e - 1 >= 0 /\ 1 >= 1 ] We thus obtain the following problem: 8: T: (1, 3) f0(a, b, c, d) -> f14(e - 1, 0, e - 2, d) [ 0 >= 0 /\ e >= 1 /\ e - 1 >= 0 /\ 1 >= 1 ] (?, 2) f10(a, b, c, d) -> f10(a - 1, b + 1, c, d) [ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a >= 1 ] (?, 1) f14(a, b, c, d) -> f14(a, b, c - 1, 0) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 /\ 0 >= e + 1 ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 /\ e >= 1 ] (?, 1) f14(a, b, c, d) -> f10(a, b, c, d) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= c ] (?, 1) f10(a, b, c, d) -> f14(a, b - 1, a - 1, d) [ a >= 0 /\ b >= 1 ] start location: f0 leaf cost: 1 By chaining the transition f14(a, b, c, d) -> f10(a, b, c, d) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= c ] with all transitions in problem 8, the following new transitions are obtained: f14(a, b, c, d) -> f10(a - 1, b + 1, c, d) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= c /\ 0 >= b /\ -b >= 0 /\ a >= 1 ] f14(a, b, c, d) -> f14(a, b - 1, a - 1, d) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= c /\ b >= 1 ] We thus obtain the following problem: 9: T: (?, 3) f14(a, b, c, d) -> f10(a - 1, b + 1, c, d) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= c /\ 0 >= b /\ -b >= 0 /\ a >= 1 ] (?, 2) f14(a, b, c, d) -> f14(a, b - 1, a - 1, d) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= c /\ b >= 1 ] (1, 3) f0(a, b, c, d) -> f14(e - 1, 0, e - 2, d) [ 0 >= 0 /\ e >= 1 /\ e - 1 >= 0 /\ 1 >= 1 ] (?, 2) f10(a, b, c, d) -> f10(a - 1, b + 1, c, d) [ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a >= 1 ] (?, 1) f14(a, b, c, d) -> f14(a, b, c - 1, 0) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 /\ 0 >= e + 1 ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 /\ e >= 1 ] (?, 1) f10(a, b, c, d) -> f14(a, b - 1, a - 1, d) [ a >= 0 /\ b >= 1 ] start location: f0 leaf cost: 1 Testing for reachability in the complexity graph removes the following transition from problem 9: f10(a, b, c, d) -> f10(a - 1, b + 1, c, d) [ a >= 0 /\ 0 >= b /\ -b >= 0 /\ a >= 1 ] We thus obtain the following problem: 10: T: (?, 1) f10(a, b, c, d) -> f14(a, b - 1, a - 1, d) [ a >= 0 /\ b >= 1 ] (?, 2) f14(a, b, c, d) -> f14(a, b - 1, a - 1, d) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= c /\ b >= 1 ] (?, 3) f14(a, b, c, d) -> f10(a - 1, b + 1, c, d) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= c /\ 0 >= b /\ -b >= 0 /\ a >= 1 ] (?, 1) f14(a, b, c, d) -> f14(a, b, c - 1, 0) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 /\ 0 >= e + 1 ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 /\ e >= 1 ] (1, 3) f0(a, b, c, d) -> f14(e - 1, 0, e - 2, d) [ 0 >= 0 /\ e >= 1 /\ e - 1 >= 0 /\ 1 >= 1 ] start location: f0 leaf cost: 1 By chaining the transition f14(a, b, c, d) -> f10(a - 1, b + 1, c, d) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= c /\ 0 >= b /\ -b >= 0 /\ a >= 1 ] with all transitions in problem 10, the following new transition is obtained: f14(a, b, c, d) -> f14(a - 1, b, a - 2, d) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= c /\ 0 >= b /\ -b >= 0 /\ a >= 1 /\ a - 1 >= 0 /\ b + 1 >= 1 ] We thus obtain the following problem: 11: T: (?, 4) f14(a, b, c, d) -> f14(a - 1, b, a - 2, d) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= c /\ 0 >= b /\ -b >= 0 /\ a >= 1 /\ a - 1 >= 0 /\ b + 1 >= 1 ] (?, 1) f10(a, b, c, d) -> f14(a, b - 1, a - 1, d) [ a >= 0 /\ b >= 1 ] (?, 2) f14(a, b, c, d) -> f14(a, b - 1, a - 1, d) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= c /\ b >= 1 ] (?, 1) f14(a, b, c, d) -> f14(a, b, c - 1, 0) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 /\ 0 >= e + 1 ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 /\ e >= 1 ] (1, 3) f0(a, b, c, d) -> f14(e - 1, 0, e - 2, d) [ 0 >= 0 /\ e >= 1 /\ e - 1 >= 0 /\ 1 >= 1 ] start location: f0 leaf cost: 1 Testing for reachability in the complexity graph removes the following transition from problem 11: f10(a, b, c, d) -> f14(a, b - 1, a - 1, d) [ a >= 0 /\ b >= 1 ] We thus obtain the following problem: 12: T: (?, 2) f14(a, b, c, d) -> f14(a, b - 1, a - 1, d) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= c /\ b >= 1 ] (?, 4) f14(a, b, c, d) -> f14(a - 1, b, a - 2, d) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= c /\ 0 >= b /\ -b >= 0 /\ a >= 1 /\ a - 1 >= 0 /\ b + 1 >= 1 ] (?, 1) f14(a, b, c, d) -> f14(a, b, c - 1, 0) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 /\ 0 >= e + 1 ] (?, 1) f14(a, b, c, d) -> f14(a - 1, b + 1, c - 1, e) [ a - c - 1 >= 0 /\ c + 1 >= 0 /\ b + c + 1 >= 0 /\ a + c + 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= 1 /\ e >= 1 ] (1, 3) f0(a, b, c, d) -> f14(e - 1, 0, e - 2, d) [ 0 >= 0 /\ e >= 1 /\ e - 1 >= 0 /\ 1 >= 1 ] start location: f0 leaf cost: 1 Complexity upper bound ? Time: 2.690 sec (SMT: 2.536 sec)