MAYBE Initial complexity problem: 1: T: (?, 1) f9(a, b, c, d) -> f15(a, 0, e, d) [ 0 >= a /\ e >= 1 ] (?, 1) f15(a, b, c, d) -> f15(a, b, c, d) [ c >= 1 ] (?, 1) f23(a, b, c, d) -> f23(a, b, c, d) (?, 1) f25(a, b, c, d) -> f28(a, b, c, d) (?, 1) f15(a, b, c, d) -> f9(e, b, c, 0) [ 0 >= c ] (?, 1) f9(a, b, c, d) -> f23(a, b, c, d) [ a >= 1 ] (1, 1) f0(a, b, c, d) -> f9(e, 0, c, 0) start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem: 2: T: (?, 1) f9(a, b, c, d) -> f15(a, 0, e, d) [ 0 >= a /\ e >= 1 ] (?, 1) f15(a, b, c, d) -> f15(a, b, c, d) [ c >= 1 ] (?, 1) f23(a, b, c, d) -> f23(a, b, c, d) (?, 1) f15(a, b, c, d) -> f9(e, b, c, 0) [ 0 >= c ] (?, 1) f9(a, b, c, d) -> f23(a, b, c, d) [ a >= 1 ] (1, 1) f0(a, b, c, d) -> f9(e, 0, c, 0) start location: f0 leaf cost: 1 Testing for reachability in the complexity graph removes the following transition from problem 2: f15(a, b, c, d) -> f9(e, b, c, 0) [ 0 >= c ] We thus obtain the following problem: 3: T: (?, 1) f23(a, b, c, d) -> f23(a, b, c, d) (?, 1) f15(a, b, c, d) -> f15(a, b, c, d) [ c >= 1 ] (?, 1) f9(a, b, c, d) -> f23(a, b, c, d) [ a >= 1 ] (?, 1) f9(a, b, c, d) -> f15(a, 0, e, d) [ 0 >= a /\ e >= 1 ] (1, 1) f0(a, b, c, d) -> f9(e, 0, c, 0) start location: f0 leaf cost: 1 Repeatedly propagating knowledge in problem 3 produces the following problem: 4: T: (?, 1) f23(a, b, c, d) -> f23(a, b, c, d) (?, 1) f15(a, b, c, d) -> f15(a, b, c, d) [ c >= 1 ] (1, 1) f9(a, b, c, d) -> f23(a, b, c, d) [ a >= 1 ] (1, 1) f9(a, b, c, d) -> f15(a, 0, e, d) [ 0 >= a /\ e >= 1 ] (1, 1) f0(a, b, c, d) -> f9(e, 0, c, 0) start location: f0 leaf cost: 1 Applied AI with 'oct' on problem 4 to obtain the following invariants: For symbol f15: -X_4 >= 0 /\ X_3 - X_4 - 1 >= 0 /\ X_2 - X_4 >= 0 /\ -X_2 - X_4 >= 0 /\ -X_1 - X_4 >= 0 /\ X_4 >= 0 /\ X_3 + X_4 - 1 >= 0 /\ X_2 + X_4 >= 0 /\ -X_2 + X_4 >= 0 /\ -X_1 + X_4 >= 0 /\ X_3 - 1 >= 0 /\ X_2 + 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_2 >= 0 /\ -X_1 + X_2 >= 0 /\ -X_1 >= 0 For symbol f23: -X_4 >= 0 /\ X_2 - X_4 >= 0 /\ -X_2 - X_4 >= 0 /\ X_1 - X_4 - 1 >= 0 /\ X_4 >= 0 /\ X_2 + X_4 >= 0 /\ -X_2 + X_4 >= 0 /\ X_1 + X_4 - 1 >= 0 /\ -X_2 >= 0 /\ X_1 - X_2 - 1 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 - 1 >= 0 /\ X_1 - 1 >= 0 For symbol f9: -X_4 >= 0 /\ X_2 - X_4 >= 0 /\ -X_2 - X_4 >= 0 /\ X_4 >= 0 /\ X_2 + X_4 >= 0 /\ -X_2 + X_4 >= 0 /\ -X_2 >= 0 /\ X_2 >= 0 This yielded the following problem: 5: T: (1, 1) f0(a, b, c, d) -> f9(e, 0, c, 0) (1, 1) f9(a, b, c, d) -> f15(a, 0, e, d) [ -d >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ d >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ -b >= 0 /\ b >= 0 /\ 0 >= a /\ e >= 1 ] (1, 1) f9(a, b, c, d) -> f23(a, b, c, d) [ -d >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ d >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ -b >= 0 /\ b >= 0 /\ a >= 1 ] (?, 1) f15(a, b, c, d) -> f15(a, b, c, d) [ -d >= 0 /\ c - d - 1 >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ -a - d >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ -a + d >= 0 /\ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ -b >= 0 /\ -a - b >= 0 /\ b >= 0 /\ -a + b >= 0 /\ -a >= 0 /\ c >= 1 ] (?, 1) f23(a, b, c, d) -> f23(a, b, c, d) [ -d >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ a + d - 1 >= 0 /\ -b >= 0 /\ a - b - 1 >= 0 /\ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 ] start location: f0 leaf cost: 1 By chaining the transition f9(a, b, c, d) -> f15(a, 0, e, d) [ -d >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ d >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ -b >= 0 /\ b >= 0 /\ 0 >= a /\ e >= 1 ] with all transitions in problem 5, the following new transition is obtained: f9(a, b, c, d) -> f15(a, 0, e, d) [ -d >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ d >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ -b >= 0 /\ b >= 0 /\ 0 >= a /\ e >= 1 /\ e - d - 1 >= 0 /\ -a - d >= 0 /\ e + d - 1 >= 0 /\ -a + d >= 0 /\ e - 1 >= 0 /\ -a + e - 1 >= 0 /\ 0 >= 0 /\ -a >= 0 ] We thus obtain the following problem: 6: T: (1, 2) f9(a, b, c, d) -> f15(a, 0, e, d) [ -d >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ d >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ -b >= 0 /\ b >= 0 /\ 0 >= a /\ e >= 1 /\ e - d - 1 >= 0 /\ -a - d >= 0 /\ e + d - 1 >= 0 /\ -a + d >= 0 /\ e - 1 >= 0 /\ -a + e - 1 >= 0 /\ 0 >= 0 /\ -a >= 0 ] (1, 1) f0(a, b, c, d) -> f9(e, 0, c, 0) (1, 1) f9(a, b, c, d) -> f23(a, b, c, d) [ -d >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ d >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ -b >= 0 /\ b >= 0 /\ a >= 1 ] (?, 1) f15(a, b, c, d) -> f15(a, b, c, d) [ -d >= 0 /\ c - d - 1 >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ -a - d >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ -a + d >= 0 /\ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ -b >= 0 /\ -a - b >= 0 /\ b >= 0 /\ -a + b >= 0 /\ -a >= 0 /\ c >= 1 ] (?, 1) f23(a, b, c, d) -> f23(a, b, c, d) [ -d >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ a + d - 1 >= 0 /\ -b >= 0 /\ a - b - 1 >= 0 /\ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 ] start location: f0 leaf cost: 1 Complexity upper bound ? Time: 0.640 sec (SMT: 0.599 sec)