YES(?, 736) Initial complexity problem: 1: T: (1, 1) f0(a, b, c, d, e, f, g) -> f43(5, 11, 0, 0, e, f, g) (?, 1) f43(a, b, c, d, e, f, g) -> f43(a, b, c, c + 1, e, f, g) [ a >= d + 1 /\ c = d ] (?, 1) f43(a, b, c, d, e, f, g) -> f43(a, b, c, d + 1, e, f, g) [ a >= d + 1 /\ c >= d + 1 ] (?, 1) f43(a, b, c, d, e, f, g) -> f43(a, b, c, d + 1, e, f, g) [ a >= d + 1 /\ d >= c + 1 ] (?, 1) f51(a, b, c, d, e, f, g) -> f54(a, b, c, d, 0, f, g) [ a >= d + 1 ] (?, 1) f54(a, b, c, d, e, f, g) -> f54(a, b, c, d, e + 1, h, i) [ b >= e + 1 ] (?, 1) f65(a, b, c, d, e, f, g) -> f71(a, b, c, d, e, h, i) [ b >= d + 1 ] (?, 1) f65(a, b, c, d, e, f, g) -> f65(a, b, c, d + 1, e, h, i) [ b >= d + 1 ] (?, 1) f75(a, b, c, d, e, f, g) -> f75(a, b, c, d + 1, e, f, g) [ a >= d + 1 ] (?, 1) f75(a, b, c, d, e, f, g) -> f71(a, b, c, d, e, f, g) [ d >= a ] (?, 1) f65(a, b, c, d, e, f, g) -> f75(a, b, c, 0, e, f, g) [ d >= b ] (?, 1) f54(a, b, c, d, e, f, g) -> f51(a, b, c, d + 1, e, f, g) [ e >= b ] (?, 1) f51(a, b, c, d, e, f, g) -> f65(a, b, c, 0, e, f, g) [ d >= a ] (?, 1) f43(a, b, c, d, e, f, g) -> f51(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, b, c, d, e]. We thus obtain the following problem: 2: T: (?, 1) f43(a, b, c, d, e) -> f51(a, b, c, 0, e) [ d >= a ] (?, 1) f51(a, b, c, d, e) -> f65(a, b, c, 0, e) [ d >= a ] (?, 1) f54(a, b, c, d, e) -> f51(a, b, c, d + 1, e) [ e >= b ] (?, 1) f65(a, b, c, d, e) -> f75(a, b, c, 0, e) [ d >= b ] (?, 1) f75(a, b, c, d, e) -> f71(a, b, c, d, e) [ d >= a ] (?, 1) f75(a, b, c, d, e) -> f75(a, b, c, d + 1, e) [ a >= d + 1 ] (?, 1) f65(a, b, c, d, e) -> f65(a, b, c, d + 1, e) [ b >= d + 1 ] (?, 1) f65(a, b, c, d, e) -> f71(a, b, c, d, e) [ b >= d + 1 ] (?, 1) f54(a, b, c, d, e) -> f54(a, b, c, d, e + 1) [ b >= e + 1 ] (?, 1) f51(a, b, c, d, e) -> f54(a, b, c, d, 0) [ a >= d + 1 ] (?, 1) f43(a, b, c, d, e) -> f43(a, b, c, d + 1, e) [ a >= d + 1 /\ d >= c + 1 ] (?, 1) f43(a, b, c, d, e) -> f43(a, b, c, d + 1, e) [ a >= d + 1 /\ c >= d + 1 ] (?, 1) f43(a, b, c, d, e) -> f43(a, b, c, c + 1, e) [ a >= d + 1 /\ c = d ] (1, 1) f0(a, b, c, d, e) -> f43(5, 11, 0, 0, e) start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (?, 1) f43(a, b, c, d, e) -> f51(a, b, c, 0, e) [ d >= a ] (?, 1) f51(a, b, c, d, e) -> f65(a, b, c, 0, e) [ d >= a ] (?, 1) f54(a, b, c, d, e) -> f51(a, b, c, d + 1, e) [ e >= b ] (?, 1) f65(a, b, c, d, e) -> f75(a, b, c, 0, e) [ d >= b ] (?, 1) f75(a, b, c, d, e) -> f75(a, b, c, d + 1, e) [ a >= d + 1 ] (?, 1) f65(a, b, c, d, e) -> f65(a, b, c, d + 1, e) [ b >= d + 1 ] (?, 1) f54(a, b, c, d, e) -> f54(a, b, c, d, e + 1) [ b >= e + 1 ] (?, 1) f51(a, b, c, d, e) -> f54(a, b, c, d, 0) [ a >= d + 1 ] (?, 1) f43(a, b, c, d, e) -> f43(a, b, c, d + 1, e) [ a >= d + 1 /\ d >= c + 1 ] (?, 1) f43(a, b, c, d, e) -> f43(a, b, c, d + 1, e) [ a >= d + 1 /\ c >= d + 1 ] (?, 1) f43(a, b, c, d, e) -> f43(a, b, c, c + 1, e) [ a >= d + 1 /\ c = d ] (1, 1) f0(a, b, c, d, e) -> f43(5, 11, 0, 0, e) start location: f0 leaf cost: 2 Testing for reachability in the complexity graph removes the following transition from problem 3: f43(a, b, c, d, e) -> f43(a, b, c, d + 1, e) [ a >= d + 1 /\ c >= d + 1 ] We thus obtain the following problem: 4: T: (?, 1) f75(a, b, c, d, e) -> f75(a, b, c, d + 1, e) [ a >= d + 1 ] (?, 1) f54(a, b, c, d, e) -> f54(a, b, c, d, e + 1) [ b >= e + 1 ] (?, 1) f54(a, b, c, d, e) -> f51(a, b, c, d + 1, e) [ e >= b ] (?, 1) f65(a, b, c, d, e) -> f65(a, b, c, d + 1, e) [ b >= d + 1 ] (?, 1) f65(a, b, c, d, e) -> f75(a, b, c, 0, e) [ d >= b ] (?, 1) f51(a, b, c, d, e) -> f54(a, b, c, d, 0) [ a >= d + 1 ] (?, 1) f51(a, b, c, d, e) -> f65(a, b, c, 0, e) [ d >= a ] (?, 1) f43(a, b, c, d, e) -> f43(a, b, c, d + 1, e) [ a >= d + 1 /\ d >= c + 1 ] (?, 1) f43(a, b, c, d, e) -> f51(a, b, c, 0, e) [ d >= a ] (?, 1) f43(a, b, c, d, e) -> f43(a, b, c, c + 1, e) [ a >= d + 1 /\ c = d ] (1, 1) f0(a, b, c, d, e) -> f43(5, 11, 0, 0, e) start location: f0 leaf cost: 2 Repeatedly propagating knowledge in problem 4 produces the following problem: 5: T: (?, 1) f75(a, b, c, d, e) -> f75(a, b, c, d + 1, e) [ a >= d + 1 ] (?, 1) f54(a, b, c, d, e) -> f54(a, b, c, d, e + 1) [ b >= e + 1 ] (?, 1) f54(a, b, c, d, e) -> f51(a, b, c, d + 1, e) [ e >= b ] (?, 1) f65(a, b, c, d, e) -> f65(a, b, c, d + 1, e) [ b >= d + 1 ] (?, 1) f65(a, b, c, d, e) -> f75(a, b, c, 0, e) [ d >= b ] (?, 1) f51(a, b, c, d, e) -> f54(a, b, c, d, 0) [ a >= d + 1 ] (?, 1) f51(a, b, c, d, e) -> f65(a, b, c, 0, e) [ d >= a ] (?, 1) f43(a, b, c, d, e) -> f43(a, b, c, d + 1, e) [ a >= d + 1 /\ d >= c + 1 ] (?, 1) f43(a, b, c, d, e) -> f51(a, b, c, 0, e) [ d >= a ] (1, 1) f43(a, b, c, d, e) -> f43(a, b, c, c + 1, e) [ a >= d + 1 /\ c = d ] (1, 1) f0(a, b, c, d, e) -> f43(5, 11, 0, 0, e) start location: f0 leaf cost: 2 Separating problem 5 produces the isolated subproblem 10001: T: (1, 0) inner_10000_start_sep(a, b, c, d, e) -> f54(a, b, c, d, 0) (?, 1) f54(a, b, c, d, e) -> f54(a, b, c, d, e + 1) [ b >= e + 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, b, c, d, e) -> f54(a, b, c, d, 0) (?, 1) f54(a, b, c, d, e) -> f54(a, b, c, d, e + 1) [ b >= e + 1 ] start location: inner_10000_start_sep leaf cost: 0 A polynomial rank function with Pol(inner_10000_start_sep) = V_2 Pol(f54) = V_2 - V_5 orients all transitions weakly and the transition f54(a, b, c, d, e) -> f54(a, b, c, d, e + 1) [ b >= e + 1 ] strictly and produces the following problem: 10002: T: (1, 0) inner_10000_start_sep(a, b, c, d, e) -> f54(a, b, c, d, 0) (b, 1) f54(a, b, c, d, e) -> f54(a, b, c, d, e + 1) [ b >= e + 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 5 produces the following problem: 6: T: (?, 0) inner_10000_in_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e) (?, b) inner_10000_in_sep(a, b, c, d, e) -> inner_10000_compl_sep(a, b, c, d, e) (?, 0) inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ b >= 0 /\ e_sep >= 0 /\ e_sep <= b ] (?, 0) inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ b >= 0 /\ e_sep < 0 /\ -e_sep <= b ] (?, 0) inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ b < 0 /\ e_sep >= 0 /\ e_sep <= -b ] (?, 0) inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ b < 0 /\ e_sep < 0 /\ -e_sep <= -b ] (?, 1) inner_10000_out_sep(a, b, c, d, e) -> f51(a, b, c, d + 1, e) [ e >= b ] (?, 1) f51(a, b, c, d, e) -> inner_10000_in_sep(a, b, c, d, 0) [ a >= d + 1 ] (1, 1) f0(a, b, c, d, e) -> f43(5, 11, 0, 0, e) (1, 1) f43(a, b, c, d, e) -> f43(a, b, c, c + 1, e) [ a >= d + 1 /\ c = d ] (?, 1) f43(a, b, c, d, e) -> f51(a, b, c, 0, e) [ d >= a ] (?, 1) f43(a, b, c, d, e) -> f43(a, b, c, d + 1, e) [ a >= d + 1 /\ d >= c + 1 ] (?, 1) f51(a, b, c, d, e) -> f65(a, b, c, 0, e) [ d >= a ] (?, 1) f65(a, b, c, d, e) -> f75(a, b, c, 0, e) [ d >= b ] (?, 1) f65(a, b, c, d, e) -> f65(a, b, c, d + 1, e) [ b >= d + 1 ] (?, 1) f75(a, b, c, d, e) -> f75(a, b, c, d + 1, e) [ a >= d + 1 ] start location: f0 leaf cost: 2 Applied AI with 'oct' on problem 6 to obtain the following invariants: For symbol f43: X_4 >= 0 /\ X_3 + X_4 >= 0 /\ -X_3 + X_4 >= 0 /\ X_2 + X_4 - 11 >= 0 /\ -X_2 + X_4 + 11 >= 0 /\ X_1 + X_4 - 5 >= 0 /\ -X_1 + X_4 + 5 >= 0 /\ -X_3 >= 0 /\ X_2 - X_3 - 11 >= 0 /\ -X_2 - X_3 + 11 >= 0 /\ X_1 - X_3 - 5 >= 0 /\ -X_1 - X_3 + 5 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 - 11 >= 0 /\ -X_2 + X_3 + 11 >= 0 /\ X_1 + X_3 - 5 >= 0 /\ -X_1 + X_3 + 5 >= 0 /\ -X_2 + 11 >= 0 /\ X_1 - X_2 + 6 >= 0 /\ -X_1 - X_2 + 16 >= 0 /\ X_2 - 11 >= 0 /\ X_1 + X_2 - 16 >= 0 /\ -X_1 + X_2 - 6 >= 0 /\ -X_1 + 5 >= 0 /\ X_1 - 5 >= 0 For symbol f51: X_4 >= 0 /\ X_3 + X_4 >= 0 /\ -X_3 + X_4 >= 0 /\ X_2 + X_4 - 11 >= 0 /\ -X_2 + X_4 + 11 >= 0 /\ X_1 + X_4 - 5 >= 0 /\ -X_1 + X_4 + 5 >= 0 /\ -X_3 >= 0 /\ X_2 - X_3 - 11 >= 0 /\ -X_2 - X_3 + 11 >= 0 /\ X_1 - X_3 - 5 >= 0 /\ -X_1 - X_3 + 5 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 - 11 >= 0 /\ -X_2 + X_3 + 11 >= 0 /\ X_1 + X_3 - 5 >= 0 /\ -X_1 + X_3 + 5 >= 0 /\ -X_2 + 11 >= 0 /\ X_1 - X_2 + 6 >= 0 /\ -X_1 - X_2 + 16 >= 0 /\ X_2 - 11 >= 0 /\ X_1 + X_2 - 16 >= 0 /\ -X_1 + X_2 - 6 >= 0 /\ -X_1 + 5 >= 0 /\ X_1 - 5 >= 0 For symbol f65: X_4 >= 0 /\ X_3 + X_4 >= 0 /\ -X_3 + X_4 >= 0 /\ X_2 + X_4 - 11 >= 0 /\ -X_2 + X_4 + 11 >= 0 /\ X_1 + X_4 - 5 >= 0 /\ -X_1 + X_4 + 5 >= 0 /\ -X_3 >= 0 /\ X_2 - X_3 - 11 >= 0 /\ -X_2 - X_3 + 11 >= 0 /\ X_1 - X_3 - 5 >= 0 /\ -X_1 - X_3 + 5 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 - 11 >= 0 /\ -X_2 + X_3 + 11 >= 0 /\ X_1 + X_3 - 5 >= 0 /\ -X_1 + X_3 + 5 >= 0 /\ -X_2 + 11 >= 0 /\ X_1 - X_2 + 6 >= 0 /\ -X_1 - X_2 + 16 >= 0 /\ X_2 - 11 >= 0 /\ X_1 + X_2 - 16 >= 0 /\ -X_1 + X_2 - 6 >= 0 /\ -X_1 + 5 >= 0 /\ X_1 - 5 >= 0 For symbol f75: X_4 >= 0 /\ X_3 + X_4 >= 0 /\ -X_3 + X_4 >= 0 /\ X_2 + X_4 - 11 >= 0 /\ -X_2 + X_4 + 11 >= 0 /\ X_1 + X_4 - 5 >= 0 /\ -X_1 + X_4 + 5 >= 0 /\ -X_3 >= 0 /\ X_2 - X_3 - 11 >= 0 /\ -X_2 - X_3 + 11 >= 0 /\ X_1 - X_3 - 5 >= 0 /\ -X_1 - X_3 + 5 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 - 11 >= 0 /\ -X_2 + X_3 + 11 >= 0 /\ X_1 + X_3 - 5 >= 0 /\ -X_1 + X_3 + 5 >= 0 /\ -X_2 + 11 >= 0 /\ X_1 - X_2 + 6 >= 0 /\ -X_1 - X_2 + 16 >= 0 /\ X_2 - 11 >= 0 /\ X_1 + X_2 - 16 >= 0 /\ -X_1 + X_2 - 6 >= 0 /\ -X_1 + 5 >= 0 /\ X_1 - 5 >= 0 For symbol inner_10000_compl_sep: -X_5 >= 0 /\ X_4 - X_5 >= 0 /\ -X_4 - X_5 + 4 >= 0 /\ X_3 - X_5 >= 0 /\ -X_3 - X_5 >= 0 /\ X_2 - X_5 - 11 >= 0 /\ -X_2 - X_5 + 11 >= 0 /\ X_1 - X_5 - 5 >= 0 /\ -X_1 - X_5 + 5 >= 0 /\ X_5 >= 0 /\ X_4 + X_5 >= 0 /\ -X_4 + X_5 + 4 >= 0 /\ X_3 + X_5 >= 0 /\ -X_3 + X_5 >= 0 /\ X_2 + X_5 - 11 >= 0 /\ -X_2 + X_5 + 11 >= 0 /\ X_1 + X_5 - 5 >= 0 /\ -X_1 + X_5 + 5 >= 0 /\ -X_4 + 4 >= 0 /\ X_3 - X_4 + 4 >= 0 /\ -X_3 - X_4 + 4 >= 0 /\ X_2 - X_4 - 7 >= 0 /\ -X_2 - X_4 + 15 >= 0 /\ X_1 - X_4 - 1 >= 0 /\ -X_1 - X_4 + 9 >= 0 /\ X_4 >= 0 /\ X_3 + X_4 >= 0 /\ -X_3 + X_4 >= 0 /\ X_2 + X_4 - 11 >= 0 /\ -X_2 + X_4 + 11 >= 0 /\ X_1 + X_4 - 5 >= 0 /\ -X_1 + X_4 + 5 >= 0 /\ -X_3 >= 0 /\ X_2 - X_3 - 11 >= 0 /\ -X_2 - X_3 + 11 >= 0 /\ X_1 - X_3 - 5 >= 0 /\ -X_1 - X_3 + 5 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 - 11 >= 0 /\ -X_2 + X_3 + 11 >= 0 /\ X_1 + X_3 - 5 >= 0 /\ -X_1 + X_3 + 5 >= 0 /\ -X_2 + 11 >= 0 /\ X_1 - X_2 + 6 >= 0 /\ -X_1 - X_2 + 16 >= 0 /\ X_2 - 11 >= 0 /\ X_1 + X_2 - 16 >= 0 /\ -X_1 + X_2 - 6 >= 0 /\ -X_1 + 5 >= 0 /\ X_1 - 5 >= 0 For symbol inner_10000_in_sep: -X_5 >= 0 /\ X_4 - X_5 >= 0 /\ -X_4 - X_5 + 4 >= 0 /\ X_3 - X_5 >= 0 /\ -X_3 - X_5 >= 0 /\ X_2 - X_5 - 11 >= 0 /\ -X_2 - X_5 + 11 >= 0 /\ X_1 - X_5 - 5 >= 0 /\ -X_1 - X_5 + 5 >= 0 /\ X_5 >= 0 /\ X_4 + X_5 >= 0 /\ -X_4 + X_5 + 4 >= 0 /\ X_3 + X_5 >= 0 /\ -X_3 + X_5 >= 0 /\ X_2 + X_5 - 11 >= 0 /\ -X_2 + X_5 + 11 >= 0 /\ X_1 + X_5 - 5 >= 0 /\ -X_1 + X_5 + 5 >= 0 /\ -X_4 + 4 >= 0 /\ X_3 - X_4 + 4 >= 0 /\ -X_3 - X_4 + 4 >= 0 /\ X_2 - X_4 - 7 >= 0 /\ -X_2 - X_4 + 15 >= 0 /\ X_1 - X_4 - 1 >= 0 /\ -X_1 - X_4 + 9 >= 0 /\ X_4 >= 0 /\ X_3 + X_4 >= 0 /\ -X_3 + X_4 >= 0 /\ X_2 + X_4 - 11 >= 0 /\ -X_2 + X_4 + 11 >= 0 /\ X_1 + X_4 - 5 >= 0 /\ -X_1 + X_4 + 5 >= 0 /\ -X_3 >= 0 /\ X_2 - X_3 - 11 >= 0 /\ -X_2 - X_3 + 11 >= 0 /\ X_1 - X_3 - 5 >= 0 /\ -X_1 - X_3 + 5 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 - 11 >= 0 /\ -X_2 + X_3 + 11 >= 0 /\ X_1 + X_3 - 5 >= 0 /\ -X_1 + X_3 + 5 >= 0 /\ -X_2 + 11 >= 0 /\ X_1 - X_2 + 6 >= 0 /\ -X_1 - X_2 + 16 >= 0 /\ X_2 - 11 >= 0 /\ X_1 + X_2 - 16 >= 0 /\ -X_1 + X_2 - 6 >= 0 /\ -X_1 + 5 >= 0 /\ X_1 - 5 >= 0 For symbol inner_10000_out_sep: -X_5 + 11 >= 0 /\ X_4 - X_5 + 11 >= 0 /\ -X_4 - X_5 + 15 >= 0 /\ X_3 - X_5 + 11 >= 0 /\ -X_3 - X_5 + 11 >= 0 /\ X_2 - X_5 >= 0 /\ -X_2 - X_5 + 22 >= 0 /\ X_1 - X_5 + 6 >= 0 /\ -X_1 - X_5 + 16 >= 0 /\ X_5 + 11 >= 0 /\ X_4 + X_5 + 11 >= 0 /\ -X_4 + X_5 + 15 >= 0 /\ X_3 + X_5 + 11 >= 0 /\ -X_3 + X_5 + 11 >= 0 /\ X_2 + X_5 >= 0 /\ -X_2 + X_5 + 22 >= 0 /\ X_1 + X_5 + 6 >= 0 /\ -X_1 + X_5 + 16 >= 0 /\ -X_4 + 4 >= 0 /\ X_3 - X_4 + 4 >= 0 /\ -X_3 - X_4 + 4 >= 0 /\ X_2 - X_4 - 7 >= 0 /\ -X_2 - X_4 + 15 >= 0 /\ X_1 - X_4 - 1 >= 0 /\ -X_1 - X_4 + 9 >= 0 /\ X_4 >= 0 /\ X_3 + X_4 >= 0 /\ -X_3 + X_4 >= 0 /\ X_2 + X_4 - 11 >= 0 /\ -X_2 + X_4 + 11 >= 0 /\ X_1 + X_4 - 5 >= 0 /\ -X_1 + X_4 + 5 >= 0 /\ -X_3 >= 0 /\ X_2 - X_3 - 11 >= 0 /\ -X_2 - X_3 + 11 >= 0 /\ X_1 - X_3 - 5 >= 0 /\ -X_1 - X_3 + 5 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 - 11 >= 0 /\ -X_2 + X_3 + 11 >= 0 /\ X_1 + X_3 - 5 >= 0 /\ -X_1 + X_3 + 5 >= 0 /\ -X_2 + 11 >= 0 /\ X_1 - X_2 + 6 >= 0 /\ -X_1 - X_2 + 16 >= 0 /\ X_2 - 11 >= 0 /\ X_1 + X_2 - 16 >= 0 /\ -X_1 + X_2 - 6 >= 0 /\ -X_1 + 5 >= 0 /\ X_1 - 5 >= 0 This yielded the following problem: 7: T: (?, 1) f75(a, b, c, d, e) -> f75(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 ] (?, 1) f65(a, b, c, d, e) -> f65(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= d + 1 ] (?, 1) f65(a, b, c, d, e) -> f75(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= b ] (?, 1) f51(a, b, c, d, e) -> f65(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= a ] (?, 1) f43(a, b, c, d, e) -> f43(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 /\ d >= c + 1 ] (?, 1) f43(a, b, c, d, e) -> f51(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= a ] (1, 1) f43(a, b, c, d, e) -> f43(a, b, c, c + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 /\ c = d ] (1, 1) f0(a, b, c, d, e) -> f43(5, 11, 0, 0, e) (?, 1) f51(a, b, c, d, e) -> inner_10000_in_sep(a, b, c, d, 0) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 ] (?, 1) inner_10000_out_sep(a, b, c, d, e) -> f51(a, b, c, d + 1, e) [ -e + 11 >= 0 /\ d - e + 11 >= 0 /\ -d - e + 15 >= 0 /\ c - e + 11 >= 0 /\ -c - e + 11 >= 0 /\ b - e >= 0 /\ -b - e + 22 >= 0 /\ a - e + 6 >= 0 /\ -a - e + 16 >= 0 /\ e + 11 >= 0 /\ d + e + 11 >= 0 /\ -d + e + 15 >= 0 /\ c + e + 11 >= 0 /\ -c + e + 11 >= 0 /\ b + e >= 0 /\ -b + e + 22 >= 0 /\ a + e + 6 >= 0 /\ -a + e + 16 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ e >= b ] (?, 0) inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b < 0 /\ e_sep < 0 /\ -e_sep <= -b ] (?, 0) inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b < 0 /\ e_sep >= 0 /\ e_sep <= -b ] (?, 0) inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= 0 /\ e_sep < 0 /\ -e_sep <= b ] (?, 0) inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= 0 /\ e_sep >= 0 /\ e_sep <= b ] (?, b) inner_10000_in_sep(a, b, c, d, e) -> inner_10000_compl_sep(a, b, c, d, e) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 ] (?, 0) inner_10000_in_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 ] start location: f0 leaf cost: 2 Testing for unsatisfiable constraints removes the following transitions from problem 7: inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b < 0 /\ e_sep < 0 /\ -e_sep <= -b ] inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b < 0 /\ e_sep >= 0 /\ e_sep <= -b ] We thus obtain the following problem: 8: T: (?, 1) f75(a, b, c, d, e) -> f75(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 ] (?, 1) f65(a, b, c, d, e) -> f65(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= d + 1 ] (?, 1) f65(a, b, c, d, e) -> f75(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= b ] (?, 1) f51(a, b, c, d, e) -> f65(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= a ] (?, 1) f43(a, b, c, d, e) -> f43(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 /\ d >= c + 1 ] (?, 1) f43(a, b, c, d, e) -> f51(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= a ] (1, 1) f43(a, b, c, d, e) -> f43(a, b, c, c + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 /\ c = d ] (1, 1) f0(a, b, c, d, e) -> f43(5, 11, 0, 0, e) (?, 1) f51(a, b, c, d, e) -> inner_10000_in_sep(a, b, c, d, 0) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 ] (?, 1) inner_10000_out_sep(a, b, c, d, e) -> f51(a, b, c, d + 1, e) [ -e + 11 >= 0 /\ d - e + 11 >= 0 /\ -d - e + 15 >= 0 /\ c - e + 11 >= 0 /\ -c - e + 11 >= 0 /\ b - e >= 0 /\ -b - e + 22 >= 0 /\ a - e + 6 >= 0 /\ -a - e + 16 >= 0 /\ e + 11 >= 0 /\ d + e + 11 >= 0 /\ -d + e + 15 >= 0 /\ c + e + 11 >= 0 /\ -c + e + 11 >= 0 /\ b + e >= 0 /\ -b + e + 22 >= 0 /\ a + e + 6 >= 0 /\ -a + e + 16 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ e >= b ] (?, 0) inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= 0 /\ e_sep < 0 /\ -e_sep <= b ] (?, 0) inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= 0 /\ e_sep >= 0 /\ e_sep <= b ] (?, b) inner_10000_in_sep(a, b, c, d, e) -> inner_10000_compl_sep(a, b, c, d, e) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 ] (?, 0) inner_10000_in_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(f75) = -1 Pol(f65) = 0 Pol(f51) = 1 Pol(f43) = 2 Pol(f0) = 2 Pol(inner_10000_in_sep) = 1 Pol(inner_10000_out_sep) = 1 Pol(inner_10000_compl_sep) = 1 orients all transitions weakly and the transition f51(a, b, c, d, e) -> f65(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= a ] strictly and produces the following problem: 9: T: (?, 1) f75(a, b, c, d, e) -> f75(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 ] (?, 1) f65(a, b, c, d, e) -> f65(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= d + 1 ] (?, 1) f65(a, b, c, d, e) -> f75(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= b ] (2, 1) f51(a, b, c, d, e) -> f65(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= a ] (?, 1) f43(a, b, c, d, e) -> f43(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 /\ d >= c + 1 ] (?, 1) f43(a, b, c, d, e) -> f51(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= a ] (1, 1) f43(a, b, c, d, e) -> f43(a, b, c, c + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 /\ c = d ] (1, 1) f0(a, b, c, d, e) -> f43(5, 11, 0, 0, e) (?, 1) f51(a, b, c, d, e) -> inner_10000_in_sep(a, b, c, d, 0) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 ] (?, 1) inner_10000_out_sep(a, b, c, d, e) -> f51(a, b, c, d + 1, e) [ -e + 11 >= 0 /\ d - e + 11 >= 0 /\ -d - e + 15 >= 0 /\ c - e + 11 >= 0 /\ -c - e + 11 >= 0 /\ b - e >= 0 /\ -b - e + 22 >= 0 /\ a - e + 6 >= 0 /\ -a - e + 16 >= 0 /\ e + 11 >= 0 /\ d + e + 11 >= 0 /\ -d + e + 15 >= 0 /\ c + e + 11 >= 0 /\ -c + e + 11 >= 0 /\ b + e >= 0 /\ -b + e + 22 >= 0 /\ a + e + 6 >= 0 /\ -a + e + 16 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ e >= b ] (?, 0) inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= 0 /\ e_sep < 0 /\ -e_sep <= b ] (?, 0) inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= 0 /\ e_sep >= 0 /\ e_sep <= b ] (?, b) inner_10000_in_sep(a, b, c, d, e) -> inner_10000_compl_sep(a, b, c, d, e) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 ] (?, 0) inner_10000_in_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(f75) = 0 Pol(f65) = 1 Pol(f51) = 1 Pol(f43) = 2 Pol(f0) = 2 Pol(inner_10000_in_sep) = 1 Pol(inner_10000_out_sep) = 1 Pol(inner_10000_compl_sep) = 1 orients all transitions weakly and the transition f65(a, b, c, d, e) -> f75(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= b ] strictly and produces the following problem: 10: T: (?, 1) f75(a, b, c, d, e) -> f75(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 ] (?, 1) f65(a, b, c, d, e) -> f65(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= d + 1 ] (2, 1) f65(a, b, c, d, e) -> f75(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= b ] (2, 1) f51(a, b, c, d, e) -> f65(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= a ] (?, 1) f43(a, b, c, d, e) -> f43(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 /\ d >= c + 1 ] (?, 1) f43(a, b, c, d, e) -> f51(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= a ] (1, 1) f43(a, b, c, d, e) -> f43(a, b, c, c + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 /\ c = d ] (1, 1) f0(a, b, c, d, e) -> f43(5, 11, 0, 0, e) (?, 1) f51(a, b, c, d, e) -> inner_10000_in_sep(a, b, c, d, 0) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 ] (?, 1) inner_10000_out_sep(a, b, c, d, e) -> f51(a, b, c, d + 1, e) [ -e + 11 >= 0 /\ d - e + 11 >= 0 /\ -d - e + 15 >= 0 /\ c - e + 11 >= 0 /\ -c - e + 11 >= 0 /\ b - e >= 0 /\ -b - e + 22 >= 0 /\ a - e + 6 >= 0 /\ -a - e + 16 >= 0 /\ e + 11 >= 0 /\ d + e + 11 >= 0 /\ -d + e + 15 >= 0 /\ c + e + 11 >= 0 /\ -c + e + 11 >= 0 /\ b + e >= 0 /\ -b + e + 22 >= 0 /\ a + e + 6 >= 0 /\ -a + e + 16 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ e >= b ] (?, 0) inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= 0 /\ e_sep < 0 /\ -e_sep <= b ] (?, 0) inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= 0 /\ e_sep >= 0 /\ e_sep <= b ] (?, b) inner_10000_in_sep(a, b, c, d, e) -> inner_10000_compl_sep(a, b, c, d, e) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 ] (?, 0) inner_10000_in_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(f75) = -24 Pol(f65) = -24 Pol(f51) = -24 Pol(f43) = 1 Pol(f0) = 1 Pol(inner_10000_in_sep) = -24 Pol(inner_10000_out_sep) = -24 Pol(inner_10000_compl_sep) = -24 orients all transitions weakly and the transition f43(a, b, c, d, e) -> f51(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= a ] strictly and produces the following problem: 11: T: (?, 1) f75(a, b, c, d, e) -> f75(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 ] (?, 1) f65(a, b, c, d, e) -> f65(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= d + 1 ] (2, 1) f65(a, b, c, d, e) -> f75(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= b ] (2, 1) f51(a, b, c, d, e) -> f65(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= a ] (?, 1) f43(a, b, c, d, e) -> f43(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 /\ d >= c + 1 ] (1, 1) f43(a, b, c, d, e) -> f51(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= a ] (1, 1) f43(a, b, c, d, e) -> f43(a, b, c, c + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 /\ c = d ] (1, 1) f0(a, b, c, d, e) -> f43(5, 11, 0, 0, e) (?, 1) f51(a, b, c, d, e) -> inner_10000_in_sep(a, b, c, d, 0) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 ] (?, 1) inner_10000_out_sep(a, b, c, d, e) -> f51(a, b, c, d + 1, e) [ -e + 11 >= 0 /\ d - e + 11 >= 0 /\ -d - e + 15 >= 0 /\ c - e + 11 >= 0 /\ -c - e + 11 >= 0 /\ b - e >= 0 /\ -b - e + 22 >= 0 /\ a - e + 6 >= 0 /\ -a - e + 16 >= 0 /\ e + 11 >= 0 /\ d + e + 11 >= 0 /\ -d + e + 15 >= 0 /\ c + e + 11 >= 0 /\ -c + e + 11 >= 0 /\ b + e >= 0 /\ -b + e + 22 >= 0 /\ a + e + 6 >= 0 /\ -a + e + 16 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ e >= b ] (?, 0) inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= 0 /\ e_sep < 0 /\ -e_sep <= b ] (?, 0) inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= 0 /\ e_sep >= 0 /\ e_sep <= b ] (?, b) inner_10000_in_sep(a, b, c, d, e) -> inner_10000_compl_sep(a, b, c, d, e) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 ] (?, 0) inner_10000_in_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(f75) = V_1 + 2*V_3 - V_4 Pol(f65) = -V_1 + V_2 + V_3 - 1 Pol(f51) = -V_1 + V_2 + 1 Pol(f43) = -V_1 + V_2 + V_3 + 1 Pol(f0) = 7 Pol(inner_10000_in_sep) = V_5 + 7 Pol(inner_10000_out_sep) = V_5 - 4 Pol(inner_10000_compl_sep) = V_5 + 7 orients all transitions weakly and the transitions inner_10000_in_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 ] inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= 0 /\ e_sep < 0 /\ -e_sep <= b ] f75(a, b, c, d, e) -> f75(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 ] strictly and produces the following problem: 12: T: (7, 1) f75(a, b, c, d, e) -> f75(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 ] (?, 1) f65(a, b, c, d, e) -> f65(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= d + 1 ] (2, 1) f65(a, b, c, d, e) -> f75(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= b ] (2, 1) f51(a, b, c, d, e) -> f65(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= a ] (?, 1) f43(a, b, c, d, e) -> f43(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 /\ d >= c + 1 ] (1, 1) f43(a, b, c, d, e) -> f51(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= a ] (1, 1) f43(a, b, c, d, e) -> f43(a, b, c, c + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 /\ c = d ] (1, 1) f0(a, b, c, d, e) -> f43(5, 11, 0, 0, e) (?, 1) f51(a, b, c, d, e) -> inner_10000_in_sep(a, b, c, d, 0) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 ] (?, 1) inner_10000_out_sep(a, b, c, d, e) -> f51(a, b, c, d + 1, e) [ -e + 11 >= 0 /\ d - e + 11 >= 0 /\ -d - e + 15 >= 0 /\ c - e + 11 >= 0 /\ -c - e + 11 >= 0 /\ b - e >= 0 /\ -b - e + 22 >= 0 /\ a - e + 6 >= 0 /\ -a - e + 16 >= 0 /\ e + 11 >= 0 /\ d + e + 11 >= 0 /\ -d + e + 15 >= 0 /\ c + e + 11 >= 0 /\ -c + e + 11 >= 0 /\ b + e >= 0 /\ -b + e + 22 >= 0 /\ a + e + 6 >= 0 /\ -a + e + 16 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ e >= b ] (7, 0) inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= 0 /\ e_sep < 0 /\ -e_sep <= b ] (?, 0) inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= 0 /\ e_sep >= 0 /\ e_sep <= b ] (?, b) inner_10000_in_sep(a, b, c, d, e) -> inner_10000_compl_sep(a, b, c, d, e) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 ] (7, 0) inner_10000_in_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(inner_10000_out_sep) = -4*V_4 + 17 Pol(f51) = -4*V_4 + 20 Pol(inner_10000_in_sep) = -4*V_4 + 19 Pol(inner_10000_compl_sep) = -4*V_4 + 18 Pol(f65) = V_2 - V_4 Pol(f43) = V_1 - V_4 and size complexities S("inner_10000_in_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 4 >= 0 /\\ c - e >= 0 /\\ -c - e >= 0 /\\ b - e - 11 >= 0 /\\ -b - e + 11 >= 0 /\\ a - e - 5 >= 0 /\\ -a - e + 5 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 4 >= 0 /\\ c + e >= 0 /\\ -c + e >= 0 /\\ b + e - 11 >= 0 /\\ -b + e + 11 >= 0 /\\ a + e - 5 >= 0 /\\ -a + e + 5 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 ]", 0-0) = 5 S("inner_10000_in_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 4 >= 0 /\\ c - e >= 0 /\\ -c - e >= 0 /\\ b - e - 11 >= 0 /\\ -b - e + 11 >= 0 /\\ a - e - 5 >= 0 /\\ -a - e + 5 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 4 >= 0 /\\ c + e >= 0 /\\ -c + e >= 0 /\\ b + e - 11 >= 0 /\\ -b + e + 11 >= 0 /\\ a + e - 5 >= 0 /\\ -a + e + 5 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 ]", 0-1) = 11 S("inner_10000_in_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 4 >= 0 /\\ c - e >= 0 /\\ -c - e >= 0 /\\ b - e - 11 >= 0 /\\ -b - e + 11 >= 0 /\\ a - e - 5 >= 0 /\\ -a - e + 5 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 4 >= 0 /\\ c + e >= 0 /\\ -c + e >= 0 /\\ b + e - 11 >= 0 /\\ -b + e + 11 >= 0 /\\ a + e - 5 >= 0 /\\ -a + e + 5 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 ]", 0-2) = 0 S("inner_10000_in_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 4 >= 0 /\\ c - e >= 0 /\\ -c - e >= 0 /\\ b - e - 11 >= 0 /\\ -b - e + 11 >= 0 /\\ a - e - 5 >= 0 /\\ -a - e + 5 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 4 >= 0 /\\ c + e >= 0 /\\ -c + e >= 0 /\\ b + e - 11 >= 0 /\\ -b + e + 11 >= 0 /\\ a + e - 5 >= 0 /\\ -a + e + 5 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 ]", 0-3) = 4 S("inner_10000_in_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 4 >= 0 /\\ c - e >= 0 /\\ -c - e >= 0 /\\ b - e - 11 >= 0 /\\ -b - e + 11 >= 0 /\\ a - e - 5 >= 0 /\\ -a - e + 5 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 4 >= 0 /\\ c + e >= 0 /\\ -c + e >= 0 /\\ b + e - 11 >= 0 /\\ -b + e + 11 >= 0 /\\ a + e - 5 >= 0 /\\ -a + e + 5 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 ]", 0-4) = 0 S("inner_10000_in_sep(a, b, c, d, e) -> inner_10000_compl_sep(a, b, c, d, e) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 4 >= 0 /\\ c - e >= 0 /\\ -c - e >= 0 /\\ b - e - 11 >= 0 /\\ -b - e + 11 >= 0 /\\ a - e - 5 >= 0 /\\ -a - e + 5 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 4 >= 0 /\\ c + e >= 0 /\\ -c + e >= 0 /\\ b + e - 11 >= 0 /\\ -b + e + 11 >= 0 /\\ a + e - 5 >= 0 /\\ -a + e + 5 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 ]", 0-0) = 5 S("inner_10000_in_sep(a, b, c, d, e) -> inner_10000_compl_sep(a, b, c, d, e) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 4 >= 0 /\\ c - e >= 0 /\\ -c - e >= 0 /\\ b - e - 11 >= 0 /\\ -b - e + 11 >= 0 /\\ a - e - 5 >= 0 /\\ -a - e + 5 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 4 >= 0 /\\ c + e >= 0 /\\ -c + e >= 0 /\\ b + e - 11 >= 0 /\\ -b + e + 11 >= 0 /\\ a + e - 5 >= 0 /\\ -a + e + 5 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 ]", 0-1) = 11 S("inner_10000_in_sep(a, b, c, d, e) -> inner_10000_compl_sep(a, b, c, d, e) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 4 >= 0 /\\ c - e >= 0 /\\ -c - e >= 0 /\\ b - e - 11 >= 0 /\\ -b - e + 11 >= 0 /\\ a - e - 5 >= 0 /\\ -a - e + 5 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 4 >= 0 /\\ c + e >= 0 /\\ -c + e >= 0 /\\ b + e - 11 >= 0 /\\ -b + e + 11 >= 0 /\\ a + e - 5 >= 0 /\\ -a + e + 5 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 ]", 0-2) = 0 S("inner_10000_in_sep(a, b, c, d, e) -> inner_10000_compl_sep(a, b, c, d, e) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 4 >= 0 /\\ c - e >= 0 /\\ -c - e >= 0 /\\ b - e - 11 >= 0 /\\ -b - e + 11 >= 0 /\\ a - e - 5 >= 0 /\\ -a - e + 5 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 4 >= 0 /\\ c + e >= 0 /\\ -c + e >= 0 /\\ b + e - 11 >= 0 /\\ -b + e + 11 >= 0 /\\ a + e - 5 >= 0 /\\ -a + e + 5 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 ]", 0-3) = 4 S("inner_10000_in_sep(a, b, c, d, e) -> inner_10000_compl_sep(a, b, c, d, e) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 4 >= 0 /\\ c - e >= 0 /\\ -c - e >= 0 /\\ b - e - 11 >= 0 /\\ -b - e + 11 >= 0 /\\ a - e - 5 >= 0 /\\ -a - e + 5 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 4 >= 0 /\\ c + e >= 0 /\\ -c + e >= 0 /\\ b + e - 11 >= 0 /\\ -b + e + 11 >= 0 /\\ a + e - 5 >= 0 /\\ -a + e + 5 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 ]", 0-4) = 0 S("inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 4 >= 0 /\\ c - e >= 0 /\\ -c - e >= 0 /\\ b - e - 11 >= 0 /\\ -b - e + 11 >= 0 /\\ a - e - 5 >= 0 /\\ -a - e + 5 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 4 >= 0 /\\ c + e >= 0 /\\ -c + e >= 0 /\\ b + e - 11 >= 0 /\\ -b + e + 11 >= 0 /\\ a + e - 5 >= 0 /\\ -a + e + 5 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ b >= 0 /\\ e_sep >= 0 /\\ e_sep <= b ]", 0-0) = 5 S("inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 4 >= 0 /\\ c - e >= 0 /\\ -c - e >= 0 /\\ b - e - 11 >= 0 /\\ -b - e + 11 >= 0 /\\ a - e - 5 >= 0 /\\ -a - e + 5 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 4 >= 0 /\\ c + e >= 0 /\\ -c + e >= 0 /\\ b + e - 11 >= 0 /\\ -b + e + 11 >= 0 /\\ a + e - 5 >= 0 /\\ -a + e + 5 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ b >= 0 /\\ e_sep >= 0 /\\ e_sep <= b ]", 0-1) = 11 S("inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 4 >= 0 /\\ c - e >= 0 /\\ -c - e >= 0 /\\ b - e - 11 >= 0 /\\ -b - e + 11 >= 0 /\\ a - e - 5 >= 0 /\\ -a - e + 5 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 4 >= 0 /\\ c + e >= 0 /\\ -c + e >= 0 /\\ b + e - 11 >= 0 /\\ -b + e + 11 >= 0 /\\ a + e - 5 >= 0 /\\ -a + e + 5 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ b >= 0 /\\ e_sep >= 0 /\\ e_sep <= b ]", 0-2) = 0 S("inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 4 >= 0 /\\ c - e >= 0 /\\ -c - e >= 0 /\\ b - e - 11 >= 0 /\\ -b - e + 11 >= 0 /\\ a - e - 5 >= 0 /\\ -a - e + 5 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 4 >= 0 /\\ c + e >= 0 /\\ -c + e >= 0 /\\ b + e - 11 >= 0 /\\ -b + e + 11 >= 0 /\\ a + e - 5 >= 0 /\\ -a + e + 5 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ b >= 0 /\\ e_sep >= 0 /\\ e_sep <= b ]", 0-3) = 4 S("inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 4 >= 0 /\\ c - e >= 0 /\\ -c - e >= 0 /\\ b - e - 11 >= 0 /\\ -b - e + 11 >= 0 /\\ a - e - 5 >= 0 /\\ -a - e + 5 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 4 >= 0 /\\ c + e >= 0 /\\ -c + e >= 0 /\\ b + e - 11 >= 0 /\\ -b + e + 11 >= 0 /\\ a + e - 5 >= 0 /\\ -a + e + 5 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ b >= 0 /\\ e_sep >= 0 /\\ e_sep <= b ]", 0-4) = 11 S("inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 4 >= 0 /\\ c - e >= 0 /\\ -c - e >= 0 /\\ b - e - 11 >= 0 /\\ -b - e + 11 >= 0 /\\ a - e - 5 >= 0 /\\ -a - e + 5 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 4 >= 0 /\\ c + e >= 0 /\\ -c + e >= 0 /\\ b + e - 11 >= 0 /\\ -b + e + 11 >= 0 /\\ a + e - 5 >= 0 /\\ -a + e + 5 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ b >= 0 /\\ e_sep < 0 /\\ -e_sep <= b ]", 0-0) = 5 S("inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 4 >= 0 /\\ c - e >= 0 /\\ -c - e >= 0 /\\ b - e - 11 >= 0 /\\ -b - e + 11 >= 0 /\\ a - e - 5 >= 0 /\\ -a - e + 5 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 4 >= 0 /\\ c + e >= 0 /\\ -c + e >= 0 /\\ b + e - 11 >= 0 /\\ -b + e + 11 >= 0 /\\ a + e - 5 >= 0 /\\ -a + e + 5 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ b >= 0 /\\ e_sep < 0 /\\ -e_sep <= b ]", 0-1) = 11 S("inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 4 >= 0 /\\ c - e >= 0 /\\ -c - e >= 0 /\\ b - e - 11 >= 0 /\\ -b - e + 11 >= 0 /\\ a - e - 5 >= 0 /\\ -a - e + 5 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 4 >= 0 /\\ c + e >= 0 /\\ -c + e >= 0 /\\ b + e - 11 >= 0 /\\ -b + e + 11 >= 0 /\\ a + e - 5 >= 0 /\\ -a + e + 5 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ b >= 0 /\\ e_sep < 0 /\\ -e_sep <= b ]", 0-2) = 0 S("inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 4 >= 0 /\\ c - e >= 0 /\\ -c - e >= 0 /\\ b - e - 11 >= 0 /\\ -b - e + 11 >= 0 /\\ a - e - 5 >= 0 /\\ -a - e + 5 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 4 >= 0 /\\ c + e >= 0 /\\ -c + e >= 0 /\\ b + e - 11 >= 0 /\\ -b + e + 11 >= 0 /\\ a + e - 5 >= 0 /\\ -a + e + 5 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ b >= 0 /\\ e_sep < 0 /\\ -e_sep <= b ]", 0-3) = 4 S("inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\\ d - e >= 0 /\\ -d - e + 4 >= 0 /\\ c - e >= 0 /\\ -c - e >= 0 /\\ b - e - 11 >= 0 /\\ -b - e + 11 >= 0 /\\ a - e - 5 >= 0 /\\ -a - e + 5 >= 0 /\\ e >= 0 /\\ d + e >= 0 /\\ -d + e + 4 >= 0 /\\ c + e >= 0 /\\ -c + e >= 0 /\\ b + e - 11 >= 0 /\\ -b + e + 11 >= 0 /\\ a + e - 5 >= 0 /\\ -a + e + 5 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ b >= 0 /\\ e_sep < 0 /\\ -e_sep <= b ]", 0-4) = 11 S("inner_10000_out_sep(a, b, c, d, e) -> f51(a, b, c, d + 1, e) [ -e + 11 >= 0 /\\ d - e + 11 >= 0 /\\ -d - e + 15 >= 0 /\\ c - e + 11 >= 0 /\\ -c - e + 11 >= 0 /\\ b - e >= 0 /\\ -b - e + 22 >= 0 /\\ a - e + 6 >= 0 /\\ -a - e + 16 >= 0 /\\ e + 11 >= 0 /\\ d + e + 11 >= 0 /\\ -d + e + 15 >= 0 /\\ c + e + 11 >= 0 /\\ -c + e + 11 >= 0 /\\ b + e >= 0 /\\ -b + e + 22 >= 0 /\\ a + e + 6 >= 0 /\\ -a + e + 16 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ e >= b ]", 0-0) = 5 S("inner_10000_out_sep(a, b, c, d, e) -> f51(a, b, c, d + 1, e) [ -e + 11 >= 0 /\\ d - e + 11 >= 0 /\\ -d - e + 15 >= 0 /\\ c - e + 11 >= 0 /\\ -c - e + 11 >= 0 /\\ b - e >= 0 /\\ -b - e + 22 >= 0 /\\ a - e + 6 >= 0 /\\ -a - e + 16 >= 0 /\\ e + 11 >= 0 /\\ d + e + 11 >= 0 /\\ -d + e + 15 >= 0 /\\ c + e + 11 >= 0 /\\ -c + e + 11 >= 0 /\\ b + e >= 0 /\\ -b + e + 22 >= 0 /\\ a + e + 6 >= 0 /\\ -a + e + 16 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ e >= b ]", 0-1) = 11 S("inner_10000_out_sep(a, b, c, d, e) -> f51(a, b, c, d + 1, e) [ -e + 11 >= 0 /\\ d - e + 11 >= 0 /\\ -d - e + 15 >= 0 /\\ c - e + 11 >= 0 /\\ -c - e + 11 >= 0 /\\ b - e >= 0 /\\ -b - e + 22 >= 0 /\\ a - e + 6 >= 0 /\\ -a - e + 16 >= 0 /\\ e + 11 >= 0 /\\ d + e + 11 >= 0 /\\ -d + e + 15 >= 0 /\\ c + e + 11 >= 0 /\\ -c + e + 11 >= 0 /\\ b + e >= 0 /\\ -b + e + 22 >= 0 /\\ a + e + 6 >= 0 /\\ -a + e + 16 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ e >= b ]", 0-2) = 0 S("inner_10000_out_sep(a, b, c, d, e) -> f51(a, b, c, d + 1, e) [ -e + 11 >= 0 /\\ d - e + 11 >= 0 /\\ -d - e + 15 >= 0 /\\ c - e + 11 >= 0 /\\ -c - e + 11 >= 0 /\\ b - e >= 0 /\\ -b - e + 22 >= 0 /\\ a - e + 6 >= 0 /\\ -a - e + 16 >= 0 /\\ e + 11 >= 0 /\\ d + e + 11 >= 0 /\\ -d + e + 15 >= 0 /\\ c + e + 11 >= 0 /\\ -c + e + 11 >= 0 /\\ b + e >= 0 /\\ -b + e + 22 >= 0 /\\ a + e + 6 >= 0 /\\ -a + e + 16 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ e >= b ]", 0-3) = 5 S("inner_10000_out_sep(a, b, c, d, e) -> f51(a, b, c, d + 1, e) [ -e + 11 >= 0 /\\ d - e + 11 >= 0 /\\ -d - e + 15 >= 0 /\\ c - e + 11 >= 0 /\\ -c - e + 11 >= 0 /\\ b - e >= 0 /\\ -b - e + 22 >= 0 /\\ a - e + 6 >= 0 /\\ -a - e + 16 >= 0 /\\ e + 11 >= 0 /\\ d + e + 11 >= 0 /\\ -d + e + 15 >= 0 /\\ c + e + 11 >= 0 /\\ -c + e + 11 >= 0 /\\ b + e >= 0 /\\ -b + e + 22 >= 0 /\\ a + e + 6 >= 0 /\\ -a + e + 16 >= 0 /\\ -d + 4 >= 0 /\\ c - d + 4 >= 0 /\\ -c - d + 4 >= 0 /\\ b - d - 7 >= 0 /\\ -b - d + 15 >= 0 /\\ a - d - 1 >= 0 /\\ -a - d + 9 >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ e >= b ]", 0-4) = 11 S("f51(a, b, c, d, e) -> inner_10000_in_sep(a, b, c, d, 0) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ a >= d + 1 ]", 0-0) = 5 S("f51(a, b, c, d, e) -> inner_10000_in_sep(a, b, c, d, 0) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ a >= d + 1 ]", 0-1) = 11 S("f51(a, b, c, d, e) -> inner_10000_in_sep(a, b, c, d, 0) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ a >= d + 1 ]", 0-2) = 0 S("f51(a, b, c, d, e) -> inner_10000_in_sep(a, b, c, d, 0) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ a >= d + 1 ]", 0-3) = 4 S("f51(a, b, c, d, e) -> inner_10000_in_sep(a, b, c, d, 0) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ a >= d + 1 ]", 0-4) = 0 S("f0(a, b, c, d, e) -> f43(5, 11, 0, 0, e)", 0-0) = 5 S("f0(a, b, c, d, e) -> f43(5, 11, 0, 0, e)", 0-1) = 11 S("f0(a, b, c, d, e) -> f43(5, 11, 0, 0, e)", 0-2) = 0 S("f0(a, b, c, d, e) -> f43(5, 11, 0, 0, e)", 0-3) = 0 S("f0(a, b, c, d, e) -> f43(5, 11, 0, 0, e)", 0-4) = e S("f43(a, b, c, d, e) -> f43(a, b, c, c + 1, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ a >= d + 1 /\\ c = d ]", 0-0) = 5 S("f43(a, b, c, d, e) -> f43(a, b, c, c + 1, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ a >= d + 1 /\\ c = d ]", 0-1) = 11 S("f43(a, b, c, d, e) -> f43(a, b, c, c + 1, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ a >= d + 1 /\\ c = d ]", 0-2) = 0 S("f43(a, b, c, d, e) -> f43(a, b, c, c + 1, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ a >= d + 1 /\\ c = d ]", 0-3) = 1 S("f43(a, b, c, d, e) -> f43(a, b, c, c + 1, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ a >= d + 1 /\\ c = d ]", 0-4) = e S("f43(a, b, c, d, e) -> f51(a, b, c, 0, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ d >= a ]", 0-0) = 5 S("f43(a, b, c, d, e) -> f51(a, b, c, 0, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ d >= a ]", 0-1) = 11 S("f43(a, b, c, d, e) -> f51(a, b, c, 0, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ d >= a ]", 0-2) = 0 S("f43(a, b, c, d, e) -> f51(a, b, c, 0, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ d >= a ]", 0-3) = 0 S("f43(a, b, c, d, e) -> f51(a, b, c, 0, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ d >= a ]", 0-4) = e S("f43(a, b, c, d, e) -> f43(a, b, c, d + 1, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ a >= d + 1 /\\ d >= c + 1 ]", 0-0) = 5 S("f43(a, b, c, d, e) -> f43(a, b, c, d + 1, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ a >= d + 1 /\\ d >= c + 1 ]", 0-1) = 11 S("f43(a, b, c, d, e) -> f43(a, b, c, d + 1, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ a >= d + 1 /\\ d >= c + 1 ]", 0-2) = 0 S("f43(a, b, c, d, e) -> f43(a, b, c, d + 1, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ a >= d + 1 /\\ d >= c + 1 ]", 0-3) = 5 S("f43(a, b, c, d, e) -> f43(a, b, c, d + 1, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ a >= d + 1 /\\ d >= c + 1 ]", 0-4) = e S("f51(a, b, c, d, e) -> f65(a, b, c, 0, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ d >= a ]", 0-0) = 5 S("f51(a, b, c, d, e) -> f65(a, b, c, 0, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ d >= a ]", 0-1) = 11 S("f51(a, b, c, d, e) -> f65(a, b, c, 0, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ d >= a ]", 0-2) = 0 S("f51(a, b, c, d, e) -> f65(a, b, c, 0, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ d >= a ]", 0-3) = 0 S("f51(a, b, c, d, e) -> f65(a, b, c, 0, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ d >= a ]", 0-4) = 11 S("f65(a, b, c, d, e) -> f75(a, b, c, 0, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ d >= b ]", 0-0) = 5 S("f65(a, b, c, d, e) -> f75(a, b, c, 0, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ d >= b ]", 0-1) = 11 S("f65(a, b, c, d, e) -> f75(a, b, c, 0, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ d >= b ]", 0-2) = 0 S("f65(a, b, c, d, e) -> f75(a, b, c, 0, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ d >= b ]", 0-3) = 0 S("f65(a, b, c, d, e) -> f75(a, b, c, 0, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ d >= b ]", 0-4) = 11 S("f65(a, b, c, d, e) -> f65(a, b, c, d + 1, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ b >= d + 1 ]", 0-0) = 5 S("f65(a, b, c, d, e) -> f65(a, b, c, d + 1, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ b >= d + 1 ]", 0-1) = 11 S("f65(a, b, c, d, e) -> f65(a, b, c, d + 1, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ b >= d + 1 ]", 0-2) = 0 S("f65(a, b, c, d, e) -> f65(a, b, c, d + 1, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ b >= d + 1 ]", 0-3) = 11 S("f65(a, b, c, d, e) -> f65(a, b, c, d + 1, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ b >= d + 1 ]", 0-4) = 11 S("f75(a, b, c, d, e) -> f75(a, b, c, d + 1, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ a >= d + 1 ]", 0-0) = 5 S("f75(a, b, c, d, e) -> f75(a, b, c, d + 1, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ a >= d + 1 ]", 0-1) = 11 S("f75(a, b, c, d, e) -> f75(a, b, c, d + 1, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ a >= d + 1 ]", 0-2) = 0 S("f75(a, b, c, d, e) -> f75(a, b, c, d + 1, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ a >= d + 1 ]", 0-3) = 5 S("f75(a, b, c, d, e) -> f75(a, b, c, d + 1, e) [ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ b + d - 11 >= 0 /\\ -b + d + 11 >= 0 /\\ a + d - 5 >= 0 /\\ -a + d + 5 >= 0 /\\ -c >= 0 /\\ b - c - 11 >= 0 /\\ -b - c + 11 >= 0 /\\ a - c - 5 >= 0 /\\ -a - c + 5 >= 0 /\\ c >= 0 /\\ b + c - 11 >= 0 /\\ -b + c + 11 >= 0 /\\ a + c - 5 >= 0 /\\ -a + c + 5 >= 0 /\\ -b + 11 >= 0 /\\ a - b + 6 >= 0 /\\ -a - b + 16 >= 0 /\\ b - 11 >= 0 /\\ a + b - 16 >= 0 /\\ -a + b - 6 >= 0 /\\ -a + 5 >= 0 /\\ a - 5 >= 0 /\\ a >= d + 1 ]", 0-4) = 11 orients the transitions inner_10000_out_sep(a, b, c, d, e) -> f51(a, b, c, d + 1, e) [ -e + 11 >= 0 /\ d - e + 11 >= 0 /\ -d - e + 15 >= 0 /\ c - e + 11 >= 0 /\ -c - e + 11 >= 0 /\ b - e >= 0 /\ -b - e + 22 >= 0 /\ a - e + 6 >= 0 /\ -a - e + 16 >= 0 /\ e + 11 >= 0 /\ d + e + 11 >= 0 /\ -d + e + 15 >= 0 /\ c + e + 11 >= 0 /\ -c + e + 11 >= 0 /\ b + e >= 0 /\ -b + e + 22 >= 0 /\ a + e + 6 >= 0 /\ -a + e + 16 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ e >= b ] inner_10000_in_sep(a, b, c, d, e) -> inner_10000_compl_sep(a, b, c, d, e) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 ] inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= 0 /\ e_sep >= 0 /\ e_sep <= b ] f65(a, b, c, d, e) -> f65(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= d + 1 ] f51(a, b, c, d, e) -> inner_10000_in_sep(a, b, c, d, 0) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 ] f43(a, b, c, d, e) -> f43(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 /\ d >= c + 1 ] weakly and the transitions inner_10000_out_sep(a, b, c, d, e) -> f51(a, b, c, d + 1, e) [ -e + 11 >= 0 /\ d - e + 11 >= 0 /\ -d - e + 15 >= 0 /\ c - e + 11 >= 0 /\ -c - e + 11 >= 0 /\ b - e >= 0 /\ -b - e + 22 >= 0 /\ a - e + 6 >= 0 /\ -a - e + 16 >= 0 /\ e + 11 >= 0 /\ d + e + 11 >= 0 /\ -d + e + 15 >= 0 /\ c + e + 11 >= 0 /\ -c + e + 11 >= 0 /\ b + e >= 0 /\ -b + e + 22 >= 0 /\ a + e + 6 >= 0 /\ -a + e + 16 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ e >= b ] inner_10000_in_sep(a, b, c, d, e) -> inner_10000_compl_sep(a, b, c, d, e) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 ] inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= 0 /\ e_sep >= 0 /\ e_sep <= b ] f65(a, b, c, d, e) -> f65(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= d + 1 ] f51(a, b, c, d, e) -> inner_10000_in_sep(a, b, c, d, 0) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 ] f43(a, b, c, d, e) -> f43(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 /\ d >= c + 1 ] strictly and produces the following problem: 13: T: (7, 1) f75(a, b, c, d, e) -> f75(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 ] (48, 1) f65(a, b, c, d, e) -> f65(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= d + 1 ] (2, 1) f65(a, b, c, d, e) -> f75(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= b ] (2, 1) f51(a, b, c, d, e) -> f65(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= a ] (48, 1) f43(a, b, c, d, e) -> f43(a, b, c, d + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 /\ d >= c + 1 ] (1, 1) f43(a, b, c, d, e) -> f51(a, b, c, 0, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ d >= a ] (1, 1) f43(a, b, c, d, e) -> f43(a, b, c, c + 1, e) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 /\ c = d ] (1, 1) f0(a, b, c, d, e) -> f43(5, 11, 0, 0, e) (48, 1) f51(a, b, c, d, e) -> inner_10000_in_sep(a, b, c, d, 0) [ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ a >= d + 1 ] (48, 1) inner_10000_out_sep(a, b, c, d, e) -> f51(a, b, c, d + 1, e) [ -e + 11 >= 0 /\ d - e + 11 >= 0 /\ -d - e + 15 >= 0 /\ c - e + 11 >= 0 /\ -c - e + 11 >= 0 /\ b - e >= 0 /\ -b - e + 22 >= 0 /\ a - e + 6 >= 0 /\ -a - e + 16 >= 0 /\ e + 11 >= 0 /\ d + e + 11 >= 0 /\ -d + e + 15 >= 0 /\ c + e + 11 >= 0 /\ -c + e + 11 >= 0 /\ b + e >= 0 /\ -b + e + 22 >= 0 /\ a + e + 6 >= 0 /\ -a + e + 16 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ e >= b ] (7, 0) inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= 0 /\ e_sep < 0 /\ -e_sep <= b ] (48, 0) inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e_sep) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 /\ b >= 0 /\ e_sep >= 0 /\ e_sep <= b ] (48, b) inner_10000_in_sep(a, b, c, d, e) -> inner_10000_compl_sep(a, b, c, d, e) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 ] (7, 0) inner_10000_in_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e) [ -e >= 0 /\ d - e >= 0 /\ -d - e + 4 >= 0 /\ c - e >= 0 /\ -c - e >= 0 /\ b - e - 11 >= 0 /\ -b - e + 11 >= 0 /\ a - e - 5 >= 0 /\ -a - e + 5 >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e + 4 >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e - 11 >= 0 /\ -b + e + 11 >= 0 /\ a + e - 5 >= 0 /\ -a + e + 5 >= 0 /\ -d + 4 >= 0 /\ c - d + 4 >= 0 /\ -c - d + 4 >= 0 /\ b - d - 7 >= 0 /\ -b - d + 15 >= 0 /\ a - d - 1 >= 0 /\ -a - d + 9 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 11 >= 0 /\ -b + d + 11 >= 0 /\ a + d - 5 >= 0 /\ -a + d + 5 >= 0 /\ -c >= 0 /\ b - c - 11 >= 0 /\ -b - c + 11 >= 0 /\ a - c - 5 >= 0 /\ -a - c + 5 >= 0 /\ c >= 0 /\ b + c - 11 >= 0 /\ -b + c + 11 >= 0 /\ a + c - 5 >= 0 /\ -a + c + 5 >= 0 /\ -b + 11 >= 0 /\ a - b + 6 >= 0 /\ -a - b + 16 >= 0 /\ b - 11 >= 0 /\ a + b - 16 >= 0 /\ -a + b - 6 >= 0 /\ -a + 5 >= 0 /\ a - 5 >= 0 ] start location: f0 leaf cost: 2 Complexity upper bound 736 Time: 3.183 sec (SMT: 2.755 sec)