YES(?, 524) Initial complexity problem: 1: T: (1, 1) f0(a, b, c, d, e, f, g) -> f12(2, h, i, 0, e, f, g) (?, 1) f12(a, b, c, d, e, f, g) -> f15(a, b, c, d, 0, f, g) [ a >= d + 1 ] (?, 1) f15(a, b, c, d, e, f, g) -> f15(a, b, c, d, e + 1, f, g) [ a >= e + 1 ] (?, 1) f23(a, b, c, d, e, f, g) -> f26(a, b, c, d, 0, f, g) [ a >= d + 1 ] (?, 1) f26(a, b, c, d, e, f, g) -> f30(a, b, c, d, e, 0, g) [ a >= e + 1 ] (?, 1) f30(a, b, c, d, e, f, g) -> f30(a, b, c, d, e, f + 1, g) [ a >= f + 1 ] (?, 1) f30(a, b, c, d, e, f, g) -> f26(a, b, c, d, e + 1, f, g) [ f >= a ] (?, 1) f26(a, b, c, d, e, f, g) -> f23(a, b, c, d + 1, e, f, g) [ e >= a ] (?, 1) f23(a, b, c, d, e, f, g) -> f52(a, b, c, d, e, f, 0) [ d >= a ] (?, 1) f23(a, b, c, d, e, f, g) -> f52(a, b, c, d, e, f, 1) [ d >= a /\ 49 >= h ] (?, 1) f23(a, b, c, d, e, f, g) -> f52(a, b, c, d, e, f, 1) [ d >= a ] (?, 1) f23(a, b, c, d, e, f, g) -> f52(a, b, c, d, e, f, 1) [ d >= a /\ 42 >= h ] (?, 1) f23(a, b, c, d, e, f, g) -> f52(a, b, c, d, e, f, 1) [ d >= a /\ 21 >= h ] (?, 1) f23(a, b, c, d, e, f, g) -> f52(a, b, c, d, e, f, 1) [ d >= a /\ 18 >= h ] (?, 1) f15(a, b, c, d, e, f, g) -> f12(a, b, c, d + 1, e, f, g) [ e >= a ] (?, 1) f12(a, b, c, d, e, f, g) -> f23(a, b, c, 0, e, f, g) [ d >= a ] start location: f0 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, d, e, f]. We thus obtain the following problem: 2: T: (?, 1) f12(a, d, e, f) -> f23(a, 0, e, f) [ d >= a ] (?, 1) f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= a ] (?, 1) f23(a, d, e, f) -> f52(a, d, e, f) [ d >= a /\ 18 >= h ] (?, 1) f23(a, d, e, f) -> f52(a, d, e, f) [ d >= a /\ 21 >= h ] (?, 1) f23(a, d, e, f) -> f52(a, d, e, f) [ d >= a /\ 42 >= h ] (?, 1) f23(a, d, e, f) -> f52(a, d, e, f) [ d >= a ] (?, 1) f23(a, d, e, f) -> f52(a, d, e, f) [ d >= a /\ 49 >= h ] (?, 1) f23(a, d, e, f) -> f52(a, d, e, f) [ d >= a ] (?, 1) f26(a, d, e, f) -> f23(a, d + 1, e, f) [ e >= a ] (?, 1) f30(a, d, e, f) -> f26(a, d, e + 1, f) [ f >= a ] (?, 1) f30(a, d, e, f) -> f30(a, d, e, f + 1) [ a >= f + 1 ] (?, 1) f26(a, d, e, f) -> f30(a, d, e, 0) [ a >= e + 1 ] (?, 1) f23(a, d, e, f) -> f26(a, d, 0, f) [ a >= d + 1 ] (?, 1) f15(a, d, e, f) -> f15(a, d, e + 1, f) [ a >= e + 1 ] (?, 1) f12(a, d, e, f) -> f15(a, d, 0, f) [ a >= d + 1 ] (1, 1) f0(a, d, e, f) -> f12(2, 0, e, f) start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (?, 1) f12(a, d, e, f) -> f23(a, 0, e, f) [ d >= a ] (?, 1) f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= a ] (?, 1) f26(a, d, e, f) -> f23(a, d + 1, e, f) [ e >= a ] (?, 1) f30(a, d, e, f) -> f26(a, d, e + 1, f) [ f >= a ] (?, 1) f30(a, d, e, f) -> f30(a, d, e, f + 1) [ a >= f + 1 ] (?, 1) f26(a, d, e, f) -> f30(a, d, e, 0) [ a >= e + 1 ] (?, 1) f23(a, d, e, f) -> f26(a, d, 0, f) [ a >= d + 1 ] (?, 1) f15(a, d, e, f) -> f15(a, d, e + 1, f) [ a >= e + 1 ] (?, 1) f12(a, d, e, f) -> f15(a, d, 0, f) [ a >= d + 1 ] (1, 1) f0(a, d, e, f) -> f12(2, 0, e, f) start location: f0 leaf cost: 6 Separating problem 3 produces the isolated subproblem 10001: T: (1, 0) inner_10000_start_sep(a, d, e, f) -> f26(a, d, 0, f) (?, 1) f26(a, d, e, f) -> f30(a, d, e, 0) [ a >= e + 1 ] (?, 1) f30(a, d, e, f) -> f30(a, d, e, f + 1) [ a >= f + 1 ] (?, 1) f30(a, d, e, f) -> f26(a, d, e + 1, f) [ f >= a ] start location: inner_10000_start_sep leaf cost: 0 === begin of proof for isolated subproblem 10001 === Initial complexity problem: 10001: T: (1, 0) inner_10000_start_sep(a, d, e, f) -> f26(a, d, 0, f) (?, 1) f26(a, d, e, f) -> f30(a, d, e, 0) [ a >= e + 1 ] (?, 1) f30(a, d, e, f) -> f30(a, d, e, f + 1) [ a >= f + 1 ] (?, 1) f30(a, d, e, f) -> f26(a, d, e + 1, f) [ f >= a ] start location: inner_10000_start_sep leaf cost: 0 Separating problem 30001 produces the isolated subproblem 10001: T: (1, 0) inner_10000_start_sep(a, d, e, f) -> f30(a, d, e, 0) (?, 1) f30(a, d, e, f) -> f30(a, d, e, f + 1) [ a >= f + 1 ] start location: inner_10000_start_sep leaf cost: 0 === begin of proof for isolated subproblem 10001 === Initial complexity problem: 10001: T: (1, 0) inner_10000_start_sep(a, d, e, f) -> f30(a, d, e, 0) (?, 1) f30(a, d, e, f) -> f30(a, d, e, f + 1) [ a >= f + 1 ] start location: inner_10000_start_sep leaf cost: 0 A polynomial rank function with Pol(inner_10000_start_sep) = V_1 Pol(f30) = V_1 - V_4 orients all transitions weakly and the transition f30(a, d, e, f) -> f30(a, d, e, f + 1) [ a >= f + 1 ] strictly and produces the following problem: 10002: T: (1, 0) inner_10000_start_sep(a, d, e, f) -> f30(a, d, e, 0) (a, 1) f30(a, d, e, f) -> f30(a, d, e, f + 1) [ a >= f + 1 ] start location: inner_10000_start_sep leaf cost: 0 === end of proof for isolated subproblem 10001 === Applying the information from the isolated subproblem 10001 to problem 30001 produces the following problem: 20002: T: (?, 0) inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) (?, a) inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f_sep) [ a >= 0 /\ f_sep >= 0 /\ f_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f_sep) [ a >= 0 /\ f_sep < 0 /\ -f_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f_sep) [ a < 0 /\ f_sep >= 0 /\ f_sep <= -a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f_sep) [ a < 0 /\ f_sep < 0 /\ -f_sep <= -a ] (?, 1) inner_10000_out_sep(a, d, e, f) -> f26(a, d, e + 1, f) [ f >= a ] (?, 1) f26(a, d, e, f) -> inner_10000_in_sep(a, d, e, 0) [ a >= e + 1 ] (1, 0) inner_10000_start_sep(a, d, e, f) -> f26(a, d, 0, f) start location: inner_10000_start_sep leaf cost: 0 Applied AI with 'oct' on problem 20002 to obtain the following invariants: For symbol f26: X_3 >= 0 For symbol inner_10000_compl_sep: -X_4 >= 0 /\ X_3 - X_4 >= 0 /\ X_1 - X_4 - 1 >= 0 /\ X_4 >= 0 /\ X_3 + X_4 >= 0 /\ X_1 + X_4 - 1 >= 0 /\ X_1 - X_3 - 1 >= 0 /\ X_3 >= 0 /\ X_1 + X_3 - 1 >= 0 /\ X_1 - 1 >= 0 For symbol inner_10000_in_sep: -X_4 >= 0 /\ X_3 - X_4 >= 0 /\ X_1 - X_4 - 1 >= 0 /\ X_4 >= 0 /\ X_3 + X_4 >= 0 /\ X_1 + X_4 - 1 >= 0 /\ X_1 - X_3 - 1 >= 0 /\ X_3 >= 0 /\ X_1 + X_3 - 1 >= 0 /\ X_1 - 1 >= 0 For symbol inner_10000_out_sep: X_1 - X_4 >= 0 /\ X_1 + X_4 >= 0 /\ X_1 - X_3 - 1 >= 0 /\ X_3 >= 0 /\ X_1 + X_3 - 1 >= 0 /\ X_1 - 1 >= 0 This yielded the following problem: 20003: T: (1, 0) inner_10000_start_sep(a, d, e, f) -> f26(a, d, 0, f) (?, 1) f26(a, d, e, f) -> inner_10000_in_sep(a, d, e, 0) [ e >= 0 /\ a >= e + 1 ] (?, 1) inner_10000_out_sep(a, d, e, f) -> f26(a, d, e + 1, f) [ a - f >= 0 /\ a + f >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 /\ f >= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f_sep) [ -f >= 0 /\ e - f >= 0 /\ a - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ a + f - 1 >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 /\ a < 0 /\ f_sep < 0 /\ -f_sep <= -a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f_sep) [ -f >= 0 /\ e - f >= 0 /\ a - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ a + f - 1 >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 /\ a < 0 /\ f_sep >= 0 /\ f_sep <= -a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f_sep) [ -f >= 0 /\ e - f >= 0 /\ a - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ a + f - 1 >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 /\ a >= 0 /\ f_sep < 0 /\ -f_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f_sep) [ -f >= 0 /\ e - f >= 0 /\ a - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ a + f - 1 >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 /\ a >= 0 /\ f_sep >= 0 /\ f_sep <= a ] (?, a) inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -f >= 0 /\ e - f >= 0 /\ a - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ a + f - 1 >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 ] (?, 0) inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -f >= 0 /\ e - f >= 0 /\ a - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ a + f - 1 >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 ] start location: inner_10000_start_sep leaf cost: 0 Testing for unsatisfiable constraints removes the following transitions from problem 20003: inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f_sep) [ -f >= 0 /\ e - f >= 0 /\ a - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ a + f - 1 >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 /\ a < 0 /\ f_sep < 0 /\ -f_sep <= -a ] inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f_sep) [ -f >= 0 /\ e - f >= 0 /\ a - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ a + f - 1 >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 /\ a < 0 /\ f_sep >= 0 /\ f_sep <= -a ] We thus obtain the following problem: 20004: T: (1, 0) inner_10000_start_sep(a, d, e, f) -> f26(a, d, 0, f) (?, 1) f26(a, d, e, f) -> inner_10000_in_sep(a, d, e, 0) [ e >= 0 /\ a >= e + 1 ] (?, 1) inner_10000_out_sep(a, d, e, f) -> f26(a, d, e + 1, f) [ a - f >= 0 /\ a + f >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 /\ f >= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f_sep) [ -f >= 0 /\ e - f >= 0 /\ a - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ a + f - 1 >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 /\ a >= 0 /\ f_sep < 0 /\ -f_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f_sep) [ -f >= 0 /\ e - f >= 0 /\ a - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ a + f - 1 >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 /\ a >= 0 /\ f_sep >= 0 /\ f_sep <= a ] (?, a) inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -f >= 0 /\ e - f >= 0 /\ a - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ a + f - 1 >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 ] (?, 0) inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -f >= 0 /\ e - f >= 0 /\ a - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ a + f - 1 >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 ] start location: inner_10000_start_sep leaf cost: 0 A polynomial rank function with Pol(inner_10000_start_sep) = 5*V_1 - 1 Pol(f26) = 5*V_1 - 4*V_3 - 1 Pol(inner_10000_in_sep) = 5*V_1 - 4*V_3 - 2 Pol(inner_10000_out_sep) = 5*V_1 - 4*V_3 - 4 Pol(inner_10000_compl_sep) = 5*V_1 - 4*V_3 - 3 orients all transitions weakly and the transitions inner_10000_out_sep(a, d, e, f) -> f26(a, d, e + 1, f) [ a - f >= 0 /\ a + f >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 /\ f >= a ] inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -f >= 0 /\ e - f >= 0 /\ a - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ a + f - 1 >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 ] inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -f >= 0 /\ e - f >= 0 /\ a - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ a + f - 1 >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 ] inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f_sep) [ -f >= 0 /\ e - f >= 0 /\ a - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ a + f - 1 >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 /\ a >= 0 /\ f_sep < 0 /\ -f_sep <= a ] inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f_sep) [ -f >= 0 /\ e - f >= 0 /\ a - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ a + f - 1 >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 /\ a >= 0 /\ f_sep >= 0 /\ f_sep <= a ] f26(a, d, e, f) -> inner_10000_in_sep(a, d, e, 0) [ e >= 0 /\ a >= e + 1 ] strictly and produces the following problem: 20005: T: (1, 0) inner_10000_start_sep(a, d, e, f) -> f26(a, d, 0, f) (5*a + 1, 1) f26(a, d, e, f) -> inner_10000_in_sep(a, d, e, 0) [ e >= 0 /\ a >= e + 1 ] (5*a + 1, 1) inner_10000_out_sep(a, d, e, f) -> f26(a, d, e + 1, f) [ a - f >= 0 /\ a + f >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 /\ f >= a ] (5*a + 1, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f_sep) [ -f >= 0 /\ e - f >= 0 /\ a - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ a + f - 1 >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 /\ a >= 0 /\ f_sep < 0 /\ -f_sep <= a ] (5*a + 1, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f_sep) [ -f >= 0 /\ e - f >= 0 /\ a - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ a + f - 1 >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 /\ a >= 0 /\ f_sep >= 0 /\ f_sep <= a ] (5*a + 1, a) inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -f >= 0 /\ e - f >= 0 /\ a - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ a + f - 1 >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 ] (5*a + 1, 0) inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -f >= 0 /\ e - f >= 0 /\ a - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ a + f - 1 >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ a + e - 1 >= 0 /\ a - 1 >= 0 ] start location: inner_10000_start_sep leaf cost: 0 === end of proof for isolated subproblem 10001 === Applying the information from the isolated subproblem 10001 to problem 3 produces the following problem: 4: T: (?, 0) inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) (?, 11*a + 5*a^2 + 2) inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ f >= 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep >= 0 /\ f_sep <= f + a /\ e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ f >= 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep < 0 /\ f_sep <= f + a /\ -e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ f >= 0 /\ f_sep >= 0 /\ a < 0 /\ e_sep >= 0 /\ f_sep <= f - a /\ e_sep <= -a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ f >= 0 /\ f_sep >= 0 /\ a < 0 /\ e_sep < 0 /\ f_sep <= f - a /\ -e_sep <= -a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ f >= 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep >= 0 /\ -f_sep <= f + a /\ e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ f >= 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep < 0 /\ -f_sep <= f + a /\ -e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ f >= 0 /\ f_sep < 0 /\ a < 0 /\ e_sep >= 0 /\ -f_sep <= f - a /\ e_sep <= -a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ f >= 0 /\ f_sep < 0 /\ a < 0 /\ e_sep < 0 /\ -f_sep <= f - a /\ -e_sep <= -a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ f < 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep >= 0 /\ f_sep <= -f + a /\ e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ f < 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep < 0 /\ f_sep <= -f + a /\ -e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ f < 0 /\ f_sep >= 0 /\ a < 0 /\ e_sep >= 0 /\ f_sep <= -f - a /\ e_sep <= -a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ f < 0 /\ f_sep >= 0 /\ a < 0 /\ e_sep < 0 /\ f_sep <= -f - a /\ -e_sep <= -a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ f < 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep >= 0 /\ -f_sep <= -f + a /\ e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ f < 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep < 0 /\ -f_sep <= -f + a /\ -e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ f < 0 /\ f_sep < 0 /\ a < 0 /\ e_sep >= 0 /\ -f_sep <= -f - a /\ e_sep <= -a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ f < 0 /\ f_sep < 0 /\ a < 0 /\ e_sep < 0 /\ -f_sep <= -f - a /\ -e_sep <= -a ] (?, 1) inner_10000_out_sep(a, d, e, f) -> f23(a, d + 1, e, f) [ e >= a ] (?, 1) f23(a, d, e, f) -> inner_10000_in_sep(a, d, 0, f) [ a >= d + 1 ] (1, 1) f0(a, d, e, f) -> f12(2, 0, e, f) (?, 1) f12(a, d, e, f) -> f15(a, d, 0, f) [ a >= d + 1 ] (?, 1) f15(a, d, e, f) -> f15(a, d, e + 1, f) [ a >= e + 1 ] (?, 1) f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= a ] (?, 1) f12(a, d, e, f) -> f23(a, 0, e, f) [ d >= a ] start location: f0 leaf cost: 6 Applied AI with 'oct' on problem 4 to obtain the following invariants: For symbol f12: X_2 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ -X_1 + X_2 + 2 >= 0 /\ -X_1 + 2 >= 0 /\ X_1 - 2 >= 0 For symbol f15: X_3 >= 0 /\ X_2 + X_3 >= 0 /\ X_1 + X_3 - 2 >= 0 /\ -X_1 + X_3 + 2 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ -X_1 + X_2 + 2 >= 0 /\ -X_1 + 2 >= 0 /\ X_1 - 2 >= 0 For symbol f23: X_2 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ -X_1 + X_2 + 2 >= 0 /\ -X_1 + 2 >= 0 /\ X_1 - 2 >= 0 For symbol inner_10000_compl_sep: -X_3 >= 0 /\ X_2 - X_3 >= 0 /\ -X_2 - X_3 + 1 >= 0 /\ X_1 - X_3 - 2 >= 0 /\ -X_1 - X_3 + 2 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 >= 0 /\ -X_2 + X_3 + 1 >= 0 /\ X_1 + X_3 - 2 >= 0 /\ -X_1 + X_3 + 2 >= 0 /\ -X_2 + 1 >= 0 /\ X_1 - X_2 - 1 >= 0 /\ -X_1 - X_2 + 3 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ -X_1 + X_2 + 2 >= 0 /\ -X_1 + 2 >= 0 /\ X_1 - 2 >= 0 For symbol inner_10000_in_sep: -X_3 >= 0 /\ X_2 - X_3 >= 0 /\ -X_2 - X_3 + 1 >= 0 /\ X_1 - X_3 - 2 >= 0 /\ -X_1 - X_3 + 2 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 >= 0 /\ -X_2 + X_3 + 1 >= 0 /\ X_1 + X_3 - 2 >= 0 /\ -X_1 + X_3 + 2 >= 0 /\ -X_2 + 1 >= 0 /\ X_1 - X_2 - 1 >= 0 /\ -X_1 - X_2 + 3 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ -X_1 + X_2 + 2 >= 0 /\ -X_1 + 2 >= 0 /\ X_1 - 2 >= 0 For symbol inner_10000_out_sep: -X_3 + 2 >= 0 /\ X_2 - X_3 + 2 >= 0 /\ -X_2 - X_3 + 3 >= 0 /\ X_1 - X_3 >= 0 /\ -X_1 - X_3 + 4 >= 0 /\ X_3 + 2 >= 0 /\ X_2 + X_3 + 2 >= 0 /\ -X_2 + X_3 + 3 >= 0 /\ X_1 + X_3 >= 0 /\ -X_1 + X_3 + 4 >= 0 /\ -X_2 + 1 >= 0 /\ X_1 - X_2 - 1 >= 0 /\ -X_1 - X_2 + 3 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ -X_1 + X_2 + 2 >= 0 /\ -X_1 + 2 >= 0 /\ X_1 - 2 >= 0 This yielded the following problem: 5: T: (?, 1) f12(a, d, e, f) -> f23(a, 0, e, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ d >= a ] (?, 1) f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= 0 /\ d + e >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ e >= a ] (?, 1) f15(a, d, e, f) -> f15(a, d, e + 1, f) [ e >= 0 /\ d + e >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= e + 1 ] (?, 1) f12(a, d, e, f) -> f15(a, d, 0, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= d + 1 ] (1, 1) f0(a, d, e, f) -> f12(2, 0, e, f) (?, 1) f23(a, d, e, f) -> inner_10000_in_sep(a, d, 0, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= d + 1 ] (?, 1) inner_10000_out_sep(a, d, e, f) -> f23(a, d + 1, e, f) [ -e + 2 >= 0 /\ d - e + 2 >= 0 /\ -d - e + 3 >= 0 /\ a - e >= 0 /\ -a - e + 4 >= 0 /\ e + 2 >= 0 /\ d + e + 2 >= 0 /\ -d + e + 3 >= 0 /\ a + e >= 0 /\ -a + e + 4 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ e >= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep < 0 /\ a < 0 /\ e_sep < 0 /\ -f_sep <= -f - a /\ -e_sep <= -a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep < 0 /\ a < 0 /\ e_sep >= 0 /\ -f_sep <= -f - a /\ e_sep <= -a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep < 0 /\ -f_sep <= -f + a /\ -e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep >= 0 /\ -f_sep <= -f + a /\ e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep >= 0 /\ a < 0 /\ e_sep < 0 /\ f_sep <= -f - a /\ -e_sep <= -a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep >= 0 /\ a < 0 /\ e_sep >= 0 /\ f_sep <= -f - a /\ e_sep <= -a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep < 0 /\ f_sep <= -f + a /\ -e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep >= 0 /\ f_sep <= -f + a /\ e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep < 0 /\ a < 0 /\ e_sep < 0 /\ -f_sep <= f - a /\ -e_sep <= -a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep < 0 /\ a < 0 /\ e_sep >= 0 /\ -f_sep <= f - a /\ e_sep <= -a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep < 0 /\ -f_sep <= f + a /\ -e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep >= 0 /\ -f_sep <= f + a /\ e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep >= 0 /\ a < 0 /\ e_sep < 0 /\ f_sep <= f - a /\ -e_sep <= -a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep >= 0 /\ a < 0 /\ e_sep >= 0 /\ f_sep <= f - a /\ e_sep <= -a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep < 0 /\ f_sep <= f + a /\ -e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep >= 0 /\ f_sep <= f + a /\ e_sep <= a ] (?, 11*a + 5*a^2 + 2) inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 ] (?, 0) inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 ] start location: f0 leaf cost: 6 Testing for unsatisfiable constraints removes the following transitions from problem 5: inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep < 0 /\ a < 0 /\ e_sep < 0 /\ -f_sep <= -f - a /\ -e_sep <= -a ] inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep < 0 /\ a < 0 /\ e_sep >= 0 /\ -f_sep <= -f - a /\ e_sep <= -a ] inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep >= 0 /\ a < 0 /\ e_sep < 0 /\ f_sep <= -f - a /\ -e_sep <= -a ] inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep >= 0 /\ a < 0 /\ e_sep >= 0 /\ f_sep <= -f - a /\ e_sep <= -a ] inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep < 0 /\ a < 0 /\ e_sep < 0 /\ -f_sep <= f - a /\ -e_sep <= -a ] inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep < 0 /\ a < 0 /\ e_sep >= 0 /\ -f_sep <= f - a /\ e_sep <= -a ] inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep >= 0 /\ a < 0 /\ e_sep < 0 /\ f_sep <= f - a /\ -e_sep <= -a ] inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep >= 0 /\ a < 0 /\ e_sep >= 0 /\ f_sep <= f - a /\ e_sep <= -a ] We thus obtain the following problem: 6: T: (?, 1) f12(a, d, e, f) -> f23(a, 0, e, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ d >= a ] (?, 1) f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= 0 /\ d + e >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ e >= a ] (?, 1) f15(a, d, e, f) -> f15(a, d, e + 1, f) [ e >= 0 /\ d + e >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= e + 1 ] (?, 1) f12(a, d, e, f) -> f15(a, d, 0, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= d + 1 ] (1, 1) f0(a, d, e, f) -> f12(2, 0, e, f) (?, 1) f23(a, d, e, f) -> inner_10000_in_sep(a, d, 0, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= d + 1 ] (?, 1) inner_10000_out_sep(a, d, e, f) -> f23(a, d + 1, e, f) [ -e + 2 >= 0 /\ d - e + 2 >= 0 /\ -d - e + 3 >= 0 /\ a - e >= 0 /\ -a - e + 4 >= 0 /\ e + 2 >= 0 /\ d + e + 2 >= 0 /\ -d + e + 3 >= 0 /\ a + e >= 0 /\ -a + e + 4 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ e >= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep < 0 /\ -f_sep <= -f + a /\ -e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep >= 0 /\ -f_sep <= -f + a /\ e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep < 0 /\ f_sep <= -f + a /\ -e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep >= 0 /\ f_sep <= -f + a /\ e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep < 0 /\ -f_sep <= f + a /\ -e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep >= 0 /\ -f_sep <= f + a /\ e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep < 0 /\ f_sep <= f + a /\ -e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep >= 0 /\ f_sep <= f + a /\ e_sep <= a ] (?, 11*a + 5*a^2 + 2) inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 ] (?, 0) inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 ] start location: f0 leaf cost: 6 A polynomial rank function with Pol(f12) = 1 Pol(f23) = -3 Pol(f15) = 1 Pol(f0) = 1 Pol(inner_10000_in_sep) = -3 Pol(inner_10000_out_sep) = -3 Pol(inner_10000_compl_sep) = -3 orients all transitions weakly and the transition f12(a, d, e, f) -> f23(a, 0, e, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ d >= a ] strictly and produces the following problem: 7: T: (1, 1) f12(a, d, e, f) -> f23(a, 0, e, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ d >= a ] (?, 1) f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= 0 /\ d + e >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ e >= a ] (?, 1) f15(a, d, e, f) -> f15(a, d, e + 1, f) [ e >= 0 /\ d + e >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= e + 1 ] (?, 1) f12(a, d, e, f) -> f15(a, d, 0, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= d + 1 ] (1, 1) f0(a, d, e, f) -> f12(2, 0, e, f) (?, 1) f23(a, d, e, f) -> inner_10000_in_sep(a, d, 0, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= d + 1 ] (?, 1) inner_10000_out_sep(a, d, e, f) -> f23(a, d + 1, e, f) [ -e + 2 >= 0 /\ d - e + 2 >= 0 /\ -d - e + 3 >= 0 /\ a - e >= 0 /\ -a - e + 4 >= 0 /\ e + 2 >= 0 /\ d + e + 2 >= 0 /\ -d + e + 3 >= 0 /\ a + e >= 0 /\ -a + e + 4 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ e >= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep < 0 /\ -f_sep <= -f + a /\ -e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep >= 0 /\ -f_sep <= -f + a /\ e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep < 0 /\ f_sep <= -f + a /\ -e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep >= 0 /\ f_sep <= -f + a /\ e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep < 0 /\ -f_sep <= f + a /\ -e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep >= 0 /\ -f_sep <= f + a /\ e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep < 0 /\ f_sep <= f + a /\ -e_sep <= a ] (?, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep >= 0 /\ f_sep <= f + a /\ e_sep <= a ] (?, 11*a + 5*a^2 + 2) inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 ] (?, 0) inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 ] start location: f0 leaf cost: 6 A polynomial rank function with Pol(f12) = V_1 + 8 Pol(f23) = V_1 - 5*V_2 + 8 Pol(f15) = V_1 + 8 Pol(f0) = 10 Pol(inner_10000_in_sep) = V_1 - 5*V_2 + 7 Pol(inner_10000_out_sep) = V_1 - 5*V_2 + 4 Pol(inner_10000_compl_sep) = V_1 - 5*V_2 + 6 orients all transitions weakly and the transitions inner_10000_out_sep(a, d, e, f) -> f23(a, d + 1, e, f) [ -e + 2 >= 0 /\ d - e + 2 >= 0 /\ -d - e + 3 >= 0 /\ a - e >= 0 /\ -a - e + 4 >= 0 /\ e + 2 >= 0 /\ d + e + 2 >= 0 /\ -d + e + 3 >= 0 /\ a + e >= 0 /\ -a + e + 4 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ e >= a ] inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 ] inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 ] inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep < 0 /\ -f_sep <= -f + a /\ -e_sep <= a ] inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep >= 0 /\ -f_sep <= -f + a /\ e_sep <= a ] inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep < 0 /\ f_sep <= -f + a /\ -e_sep <= a ] inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep >= 0 /\ f_sep <= -f + a /\ e_sep <= a ] inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep < 0 /\ -f_sep <= f + a /\ -e_sep <= a ] inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep >= 0 /\ -f_sep <= f + a /\ e_sep <= a ] inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep < 0 /\ f_sep <= f + a /\ -e_sep <= a ] inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep >= 0 /\ f_sep <= f + a /\ e_sep <= a ] f23(a, d, e, f) -> inner_10000_in_sep(a, d, 0, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= d + 1 ] strictly and produces the following problem: 8: T: (1, 1) f12(a, d, e, f) -> f23(a, 0, e, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ d >= a ] (?, 1) f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= 0 /\ d + e >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ e >= a ] (?, 1) f15(a, d, e, f) -> f15(a, d, e + 1, f) [ e >= 0 /\ d + e >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= e + 1 ] (?, 1) f12(a, d, e, f) -> f15(a, d, 0, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= d + 1 ] (1, 1) f0(a, d, e, f) -> f12(2, 0, e, f) (10, 1) f23(a, d, e, f) -> inner_10000_in_sep(a, d, 0, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= d + 1 ] (10, 1) inner_10000_out_sep(a, d, e, f) -> f23(a, d + 1, e, f) [ -e + 2 >= 0 /\ d - e + 2 >= 0 /\ -d - e + 3 >= 0 /\ a - e >= 0 /\ -a - e + 4 >= 0 /\ e + 2 >= 0 /\ d + e + 2 >= 0 /\ -d + e + 3 >= 0 /\ a + e >= 0 /\ -a + e + 4 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ e >= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep < 0 /\ -f_sep <= -f + a /\ -e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep >= 0 /\ -f_sep <= -f + a /\ e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep < 0 /\ f_sep <= -f + a /\ -e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep >= 0 /\ f_sep <= -f + a /\ e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep < 0 /\ -f_sep <= f + a /\ -e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep >= 0 /\ -f_sep <= f + a /\ e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep < 0 /\ f_sep <= f + a /\ -e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep >= 0 /\ f_sep <= f + a /\ e_sep <= a ] (10, 11*a + 5*a^2 + 2) inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 ] (10, 0) inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 ] start location: f0 leaf cost: 6 A polynomial rank function with Pol(f15) = 5*V_1 - 5*V_2 - 8 Pol(f12) = 5*V_1 - 5*V_2 - 4 and size complexities S("inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-0) = 2 S("inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-1) = 1 S("inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-2) = 0 S("inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-3) = ? S("inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-0) = 2 S("inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-1) = 1 S("inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-2) = 0 S("inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= f + a /\\ e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= f + a /\\ e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= f + a /\\ e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= f + a /\\ e_sep <= a ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= f + a /\\ -e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= f + a /\\ -e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= f + a /\\ -e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= f + a /\\ -e_sep <= a ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= f + a /\\ e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= f + a /\\ e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= f + a /\\ e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= f + a /\\ e_sep <= a ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= f + a /\\ -e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= f + a /\\ -e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= f + a /\\ -e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= f + a /\\ -e_sep <= a ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= -f + a /\\ e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= -f + a /\\ e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= -f + a /\\ e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= -f + a /\\ e_sep <= a ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= -f + a /\\ -e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= -f + a /\\ -e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= -f + a /\\ -e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= -f + a /\\ -e_sep <= a ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= -f + a /\\ e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= -f + a /\\ e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= -f + a /\\ e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= -f + a /\\ e_sep <= a ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= -f + a /\\ -e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= -f + a /\\ -e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= -f + a /\\ -e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= -f + a /\\ -e_sep <= a ]", 0-3) = ? S("inner_10000_out_sep(a, d, e, f) -> f23(a, d + 1, e, f) [ -e + 2 >= 0 /\\ d - e + 2 >= 0 /\\ -d - e + 3 >= 0 /\\ a - e >= 0 /\\ -a - e + 4 >= 0 /\\ e + 2 >= 0 /\\ d + e + 2 >= 0 /\\ -d + e + 3 >= 0 /\\ a + e >= 0 /\\ -a + e + 4 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-0) = 2 S("inner_10000_out_sep(a, d, e, f) -> f23(a, d + 1, e, f) [ -e + 2 >= 0 /\\ d - e + 2 >= 0 /\\ -d - e + 3 >= 0 /\\ a - e >= 0 /\\ -a - e + 4 >= 0 /\\ e + 2 >= 0 /\\ d + e + 2 >= 0 /\\ -d + e + 3 >= 0 /\\ a + e >= 0 /\\ -a + e + 4 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-1) = 2 S("inner_10000_out_sep(a, d, e, f) -> f23(a, d + 1, e, f) [ -e + 2 >= 0 /\\ d - e + 2 >= 0 /\\ -d - e + 3 >= 0 /\\ a - e >= 0 /\\ -a - e + 4 >= 0 /\\ e + 2 >= 0 /\\ d + e + 2 >= 0 /\\ -d + e + 3 >= 0 /\\ a + e >= 0 /\\ -a + e + 4 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-2) = 2 S("inner_10000_out_sep(a, d, e, f) -> f23(a, d + 1, e, f) [ -e + 2 >= 0 /\\ d - e + 2 >= 0 /\\ -d - e + 3 >= 0 /\\ a - e >= 0 /\\ -a - e + 4 >= 0 /\\ e + 2 >= 0 /\\ d + e + 2 >= 0 /\\ -d + e + 3 >= 0 /\\ a + e >= 0 /\\ -a + e + 4 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-3) = ? S("f23(a, d, e, f) -> inner_10000_in_sep(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-0) = 2 S("f23(a, d, e, f) -> inner_10000_in_sep(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-1) = 1 S("f23(a, d, e, f) -> inner_10000_in_sep(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-2) = 0 S("f23(a, d, e, f) -> inner_10000_in_sep(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-3) = ? S("f0(a, d, e, f) -> f12(2, 0, e, f)", 0-0) = 2 S("f0(a, d, e, f) -> f12(2, 0, e, f)", 0-1) = 0 S("f0(a, d, e, f) -> f12(2, 0, e, f)", 0-2) = e S("f0(a, d, e, f) -> f12(2, 0, e, f)", 0-3) = f S("f12(a, d, e, f) -> f15(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-0) = 2 S("f12(a, d, e, f) -> f15(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-1) = 1 S("f12(a, d, e, f) -> f15(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-2) = 0 S("f12(a, d, e, f) -> f15(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-3) = f S("f15(a, d, e, f) -> f15(a, d, e + 1, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= e + 1 ]", 0-0) = 2 S("f15(a, d, e, f) -> f15(a, d, e + 1, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= e + 1 ]", 0-1) = 1 S("f15(a, d, e, f) -> f15(a, d, e + 1, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= e + 1 ]", 0-2) = 2 S("f15(a, d, e, f) -> f15(a, d, e + 1, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= e + 1 ]", 0-3) = f S("f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-0) = 2 S("f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-1) = 2 S("f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-2) = 2 S("f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-3) = f S("f12(a, d, e, f) -> f23(a, 0, e, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ d >= a ]", 0-0) = 2 S("f12(a, d, e, f) -> f23(a, 0, e, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ d >= a ]", 0-1) = 0 S("f12(a, d, e, f) -> f23(a, 0, e, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ d >= a ]", 0-2) = 2 S("f12(a, d, e, f) -> f23(a, 0, e, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ d >= a ]", 0-3) = f orients the transitions f15(a, d, e, f) -> f15(a, d, e + 1, f) [ e >= 0 /\ d + e >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= e + 1 ] f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= 0 /\ d + e >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ e >= a ] f12(a, d, e, f) -> f15(a, d, 0, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= d + 1 ] weakly and the transition f12(a, d, e, f) -> f15(a, d, 0, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= d + 1 ] strictly and produces the following problem: 9: T: (1, 1) f12(a, d, e, f) -> f23(a, 0, e, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ d >= a ] (?, 1) f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= 0 /\ d + e >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ e >= a ] (?, 1) f15(a, d, e, f) -> f15(a, d, e + 1, f) [ e >= 0 /\ d + e >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= e + 1 ] (14, 1) f12(a, d, e, f) -> f15(a, d, 0, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= d + 1 ] (1, 1) f0(a, d, e, f) -> f12(2, 0, e, f) (10, 1) f23(a, d, e, f) -> inner_10000_in_sep(a, d, 0, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= d + 1 ] (10, 1) inner_10000_out_sep(a, d, e, f) -> f23(a, d + 1, e, f) [ -e + 2 >= 0 /\ d - e + 2 >= 0 /\ -d - e + 3 >= 0 /\ a - e >= 0 /\ -a - e + 4 >= 0 /\ e + 2 >= 0 /\ d + e + 2 >= 0 /\ -d + e + 3 >= 0 /\ a + e >= 0 /\ -a + e + 4 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ e >= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep < 0 /\ -f_sep <= -f + a /\ -e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep >= 0 /\ -f_sep <= -f + a /\ e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep < 0 /\ f_sep <= -f + a /\ -e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep >= 0 /\ f_sep <= -f + a /\ e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep < 0 /\ -f_sep <= f + a /\ -e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep >= 0 /\ -f_sep <= f + a /\ e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep < 0 /\ f_sep <= f + a /\ -e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep >= 0 /\ f_sep <= f + a /\ e_sep <= a ] (10, 11*a + 5*a^2 + 2) inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 ] (10, 0) inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 ] start location: f0 leaf cost: 6 A polynomial rank function with Pol(f15) = 1 Pol(f12) = 0 and size complexities S("inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-0) = 2 S("inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-1) = 1 S("inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-2) = 0 S("inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-3) = ? S("inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-0) = 2 S("inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-1) = 1 S("inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-2) = 0 S("inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= f + a /\\ e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= f + a /\\ e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= f + a /\\ e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= f + a /\\ e_sep <= a ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= f + a /\\ -e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= f + a /\\ -e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= f + a /\\ -e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= f + a /\\ -e_sep <= a ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= f + a /\\ e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= f + a /\\ e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= f + a /\\ e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= f + a /\\ e_sep <= a ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= f + a /\\ -e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= f + a /\\ -e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= f + a /\\ -e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= f + a /\\ -e_sep <= a ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= -f + a /\\ e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= -f + a /\\ e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= -f + a /\\ e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= -f + a /\\ e_sep <= a ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= -f + a /\\ -e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= -f + a /\\ -e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= -f + a /\\ -e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= -f + a /\\ -e_sep <= a ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= -f + a /\\ e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= -f + a /\\ e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= -f + a /\\ e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= -f + a /\\ e_sep <= a ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= -f + a /\\ -e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= -f + a /\\ -e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= -f + a /\\ -e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= -f + a /\\ -e_sep <= a ]", 0-3) = ? S("inner_10000_out_sep(a, d, e, f) -> f23(a, d + 1, e, f) [ -e + 2 >= 0 /\\ d - e + 2 >= 0 /\\ -d - e + 3 >= 0 /\\ a - e >= 0 /\\ -a - e + 4 >= 0 /\\ e + 2 >= 0 /\\ d + e + 2 >= 0 /\\ -d + e + 3 >= 0 /\\ a + e >= 0 /\\ -a + e + 4 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-0) = 2 S("inner_10000_out_sep(a, d, e, f) -> f23(a, d + 1, e, f) [ -e + 2 >= 0 /\\ d - e + 2 >= 0 /\\ -d - e + 3 >= 0 /\\ a - e >= 0 /\\ -a - e + 4 >= 0 /\\ e + 2 >= 0 /\\ d + e + 2 >= 0 /\\ -d + e + 3 >= 0 /\\ a + e >= 0 /\\ -a + e + 4 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-1) = 2 S("inner_10000_out_sep(a, d, e, f) -> f23(a, d + 1, e, f) [ -e + 2 >= 0 /\\ d - e + 2 >= 0 /\\ -d - e + 3 >= 0 /\\ a - e >= 0 /\\ -a - e + 4 >= 0 /\\ e + 2 >= 0 /\\ d + e + 2 >= 0 /\\ -d + e + 3 >= 0 /\\ a + e >= 0 /\\ -a + e + 4 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-2) = 2 S("inner_10000_out_sep(a, d, e, f) -> f23(a, d + 1, e, f) [ -e + 2 >= 0 /\\ d - e + 2 >= 0 /\\ -d - e + 3 >= 0 /\\ a - e >= 0 /\\ -a - e + 4 >= 0 /\\ e + 2 >= 0 /\\ d + e + 2 >= 0 /\\ -d + e + 3 >= 0 /\\ a + e >= 0 /\\ -a + e + 4 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-3) = ? S("f23(a, d, e, f) -> inner_10000_in_sep(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-0) = 2 S("f23(a, d, e, f) -> inner_10000_in_sep(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-1) = 1 S("f23(a, d, e, f) -> inner_10000_in_sep(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-2) = 0 S("f23(a, d, e, f) -> inner_10000_in_sep(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-3) = ? S("f0(a, d, e, f) -> f12(2, 0, e, f)", 0-0) = 2 S("f0(a, d, e, f) -> f12(2, 0, e, f)", 0-1) = 0 S("f0(a, d, e, f) -> f12(2, 0, e, f)", 0-2) = e S("f0(a, d, e, f) -> f12(2, 0, e, f)", 0-3) = f S("f12(a, d, e, f) -> f15(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-0) = 2 S("f12(a, d, e, f) -> f15(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-1) = 1 S("f12(a, d, e, f) -> f15(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-2) = 0 S("f12(a, d, e, f) -> f15(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-3) = f S("f15(a, d, e, f) -> f15(a, d, e + 1, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= e + 1 ]", 0-0) = 2 S("f15(a, d, e, f) -> f15(a, d, e + 1, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= e + 1 ]", 0-1) = 1 S("f15(a, d, e, f) -> f15(a, d, e + 1, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= e + 1 ]", 0-2) = 2 S("f15(a, d, e, f) -> f15(a, d, e + 1, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= e + 1 ]", 0-3) = f S("f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-0) = 2 S("f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-1) = 2 S("f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-2) = 2 S("f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-3) = f S("f12(a, d, e, f) -> f23(a, 0, e, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ d >= a ]", 0-0) = 2 S("f12(a, d, e, f) -> f23(a, 0, e, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ d >= a ]", 0-1) = 0 S("f12(a, d, e, f) -> f23(a, 0, e, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ d >= a ]", 0-2) = 2 S("f12(a, d, e, f) -> f23(a, 0, e, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ d >= a ]", 0-3) = f orients the transitions f15(a, d, e, f) -> f15(a, d, e + 1, f) [ e >= 0 /\ d + e >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= e + 1 ] f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= 0 /\ d + e >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ e >= a ] weakly and the transition f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= 0 /\ d + e >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ e >= a ] strictly and produces the following problem: 10: T: (1, 1) f12(a, d, e, f) -> f23(a, 0, e, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ d >= a ] (14, 1) f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= 0 /\ d + e >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ e >= a ] (?, 1) f15(a, d, e, f) -> f15(a, d, e + 1, f) [ e >= 0 /\ d + e >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= e + 1 ] (14, 1) f12(a, d, e, f) -> f15(a, d, 0, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= d + 1 ] (1, 1) f0(a, d, e, f) -> f12(2, 0, e, f) (10, 1) f23(a, d, e, f) -> inner_10000_in_sep(a, d, 0, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= d + 1 ] (10, 1) inner_10000_out_sep(a, d, e, f) -> f23(a, d + 1, e, f) [ -e + 2 >= 0 /\ d - e + 2 >= 0 /\ -d - e + 3 >= 0 /\ a - e >= 0 /\ -a - e + 4 >= 0 /\ e + 2 >= 0 /\ d + e + 2 >= 0 /\ -d + e + 3 >= 0 /\ a + e >= 0 /\ -a + e + 4 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ e >= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep < 0 /\ -f_sep <= -f + a /\ -e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep >= 0 /\ -f_sep <= -f + a /\ e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep < 0 /\ f_sep <= -f + a /\ -e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep >= 0 /\ f_sep <= -f + a /\ e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep < 0 /\ -f_sep <= f + a /\ -e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep >= 0 /\ -f_sep <= f + a /\ e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep < 0 /\ f_sep <= f + a /\ -e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep >= 0 /\ f_sep <= f + a /\ e_sep <= a ] (10, 11*a + 5*a^2 + 2) inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 ] (10, 0) inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 ] start location: f0 leaf cost: 6 A polynomial rank function with Pol(f15) = V_1 - V_3 and size complexities S("inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-0) = 2 S("inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-1) = 1 S("inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-2) = 0 S("inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-3) = ? S("inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-0) = 2 S("inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-1) = 1 S("inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-2) = 0 S("inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= f + a /\\ e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= f + a /\\ e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= f + a /\\ e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= f + a /\\ e_sep <= a ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= f + a /\\ -e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= f + a /\\ -e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= f + a /\\ -e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= f + a /\\ -e_sep <= a ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= f + a /\\ e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= f + a /\\ e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= f + a /\\ e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= f + a /\\ e_sep <= a ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= f + a /\\ -e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= f + a /\\ -e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= f + a /\\ -e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f >= 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= f + a /\\ -e_sep <= a ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= -f + a /\\ e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= -f + a /\\ e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= -f + a /\\ e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ f_sep <= -f + a /\\ e_sep <= a ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= -f + a /\\ -e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= -f + a /\\ -e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= -f + a /\\ -e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep >= 0 /\\ a >= 0 /\\ e_sep < 0 /\\ f_sep <= -f + a /\\ -e_sep <= a ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= -f + a /\\ e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= -f + a /\\ e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= -f + a /\\ e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep >= 0 /\\ -f_sep <= -f + a /\\ e_sep <= a ]", 0-3) = ? S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= -f + a /\\ -e_sep <= a ]", 0-0) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= -f + a /\\ -e_sep <= a ]", 0-1) = 1 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= -f + a /\\ -e_sep <= a ]", 0-2) = 2 S("inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 1 >= 0 /\\ a - e - 2 >= 0 /\\ -a - e + 2 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 1 >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ f < 0 /\\ f_sep < 0 /\\ a >= 0 /\\ e_sep < 0 /\\ -f_sep <= -f + a /\\ -e_sep <= a ]", 0-3) = ? S("inner_10000_out_sep(a, d, e, f) -> f23(a, d + 1, e, f) [ -e + 2 >= 0 /\\ d - e + 2 >= 0 /\\ -d - e + 3 >= 0 /\\ a - e >= 0 /\\ -a - e + 4 >= 0 /\\ e + 2 >= 0 /\\ d + e + 2 >= 0 /\\ -d + e + 3 >= 0 /\\ a + e >= 0 /\\ -a + e + 4 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-0) = 2 S("inner_10000_out_sep(a, d, e, f) -> f23(a, d + 1, e, f) [ -e + 2 >= 0 /\\ d - e + 2 >= 0 /\\ -d - e + 3 >= 0 /\\ a - e >= 0 /\\ -a - e + 4 >= 0 /\\ e + 2 >= 0 /\\ d + e + 2 >= 0 /\\ -d + e + 3 >= 0 /\\ a + e >= 0 /\\ -a + e + 4 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-1) = 2 S("inner_10000_out_sep(a, d, e, f) -> f23(a, d + 1, e, f) [ -e + 2 >= 0 /\\ d - e + 2 >= 0 /\\ -d - e + 3 >= 0 /\\ a - e >= 0 /\\ -a - e + 4 >= 0 /\\ e + 2 >= 0 /\\ d + e + 2 >= 0 /\\ -d + e + 3 >= 0 /\\ a + e >= 0 /\\ -a + e + 4 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-2) = 2 S("inner_10000_out_sep(a, d, e, f) -> f23(a, d + 1, e, f) [ -e + 2 >= 0 /\\ d - e + 2 >= 0 /\\ -d - e + 3 >= 0 /\\ a - e >= 0 /\\ -a - e + 4 >= 0 /\\ e + 2 >= 0 /\\ d + e + 2 >= 0 /\\ -d + e + 3 >= 0 /\\ a + e >= 0 /\\ -a + e + 4 >= 0 /\\ -d + 1 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 3 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-3) = ? S("f23(a, d, e, f) -> inner_10000_in_sep(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-0) = 2 S("f23(a, d, e, f) -> inner_10000_in_sep(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-1) = 1 S("f23(a, d, e, f) -> inner_10000_in_sep(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-2) = 0 S("f23(a, d, e, f) -> inner_10000_in_sep(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-3) = ? S("f0(a, d, e, f) -> f12(2, 0, e, f)", 0-0) = 2 S("f0(a, d, e, f) -> f12(2, 0, e, f)", 0-1) = 0 S("f0(a, d, e, f) -> f12(2, 0, e, f)", 0-2) = e S("f0(a, d, e, f) -> f12(2, 0, e, f)", 0-3) = f S("f12(a, d, e, f) -> f15(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-0) = 2 S("f12(a, d, e, f) -> f15(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-1) = 1 S("f12(a, d, e, f) -> f15(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-2) = 0 S("f12(a, d, e, f) -> f15(a, d, 0, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= d + 1 ]", 0-3) = f S("f15(a, d, e, f) -> f15(a, d, e + 1, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= e + 1 ]", 0-0) = 2 S("f15(a, d, e, f) -> f15(a, d, e + 1, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= e + 1 ]", 0-1) = 1 S("f15(a, d, e, f) -> f15(a, d, e + 1, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= e + 1 ]", 0-2) = 2 S("f15(a, d, e, f) -> f15(a, d, e + 1, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ a >= e + 1 ]", 0-3) = f S("f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-0) = 2 S("f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-1) = 2 S("f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-2) = 2 S("f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= 0 /\\ d + e >= 0 /\\ a + e - 2 >= 0 /\\ -a + e + 2 >= 0 /\\ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ e >= a ]", 0-3) = f S("f12(a, d, e, f) -> f23(a, 0, e, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ d >= a ]", 0-0) = 2 S("f12(a, d, e, f) -> f23(a, 0, e, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ d >= a ]", 0-1) = 0 S("f12(a, d, e, f) -> f23(a, 0, e, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ d >= a ]", 0-2) = 2 S("f12(a, d, e, f) -> f23(a, 0, e, f) [ d >= 0 /\\ a + d - 2 >= 0 /\\ -a + d + 2 >= 0 /\\ -a + 2 >= 0 /\\ a - 2 >= 0 /\\ d >= a ]", 0-3) = f orients the transition f15(a, d, e, f) -> f15(a, d, e + 1, f) [ e >= 0 /\ d + e >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= e + 1 ] weakly and the transition f15(a, d, e, f) -> f15(a, d, e + 1, f) [ e >= 0 /\ d + e >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= e + 1 ] strictly and produces the following problem: 11: T: (1, 1) f12(a, d, e, f) -> f23(a, 0, e, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ d >= a ] (14, 1) f15(a, d, e, f) -> f12(a, d + 1, e, f) [ e >= 0 /\ d + e >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ e >= a ] (28, 1) f15(a, d, e, f) -> f15(a, d, e + 1, f) [ e >= 0 /\ d + e >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= e + 1 ] (14, 1) f12(a, d, e, f) -> f15(a, d, 0, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= d + 1 ] (1, 1) f0(a, d, e, f) -> f12(2, 0, e, f) (10, 1) f23(a, d, e, f) -> inner_10000_in_sep(a, d, 0, f) [ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ a >= d + 1 ] (10, 1) inner_10000_out_sep(a, d, e, f) -> f23(a, d + 1, e, f) [ -e + 2 >= 0 /\ d - e + 2 >= 0 /\ -d - e + 3 >= 0 /\ a - e >= 0 /\ -a - e + 4 >= 0 /\ e + 2 >= 0 /\ d + e + 2 >= 0 /\ -d + e + 3 >= 0 /\ a + e >= 0 /\ -a + e + 4 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ e >= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep < 0 /\ -f_sep <= -f + a /\ -e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep >= 0 /\ -f_sep <= -f + a /\ e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep < 0 /\ f_sep <= -f + a /\ -e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f < 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep >= 0 /\ f_sep <= -f + a /\ e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep < 0 /\ -f_sep <= f + a /\ -e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep < 0 /\ a >= 0 /\ e_sep >= 0 /\ -f_sep <= f + a /\ e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep < 0 /\ f_sep <= f + a /\ -e_sep <= a ] (10, 0) inner_10000_compl_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e_sep, f_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 /\ f >= 0 /\ f_sep >= 0 /\ a >= 0 /\ e_sep >= 0 /\ f_sep <= f + a /\ e_sep <= a ] (10, 11*a + 5*a^2 + 2) inner_10000_in_sep(a, d, e, f) -> inner_10000_compl_sep(a, d, e, f) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 ] (10, 0) inner_10000_in_sep(a, d, e, f) -> inner_10000_out_sep(a, d, e, f) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 1 >= 0 /\ a - e - 2 >= 0 /\ -a - e + 2 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ a + e - 2 >= 0 /\ -a + e + 2 >= 0 /\ -d + 1 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 3 >= 0 /\ d >= 0 /\ a + d - 2 >= 0 /\ -a + d + 2 >= 0 /\ -a + 2 >= 0 /\ a - 2 >= 0 ] start location: f0 leaf cost: 6 Complexity upper bound 524 Time: 2.968 sec (SMT: 2.714 sec)