MAYBE Initial complexity problem: 1: T: (1, 1) f0(a, b, c, d) -> f6(1, c, c, d) (?, 1) f6(a, b, c, d) -> f6(a, e, c, e) [ b >= a + 2 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(e, b, c, e) [ b >= a + 2 /\ c >= e^2 ] (?, 1) f6(a, b, c, d) -> f16(a, b, c, d) [ a + 1 >= b ] start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem: 2: T: (1, 1) f0(a, b, c, d) -> f6(1, c, c, d) (?, 1) f6(a, b, c, d) -> f6(a, e, c, e) [ b >= a + 2 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(e, b, c, e) [ b >= a + 2 /\ c >= e^2 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c, d) -> f6(1, c, c, d) with all transitions in problem 2, the following new transitions are obtained: f0(a, b, c, d) -> f6(e, c, c, e) [ c >= 3 /\ c >= e^2 ] f0(a, b, c, d) -> f6(1, e, c, e) [ c >= 3 /\ e^2 >= c + 1 ] We thus obtain the following problem: 3: T: (1, 2) f0(a, b, c, d) -> f6(e, c, c, e) [ c >= 3 /\ c >= e^2 ] (1, 2) f0(a, b, c, d) -> f6(1, e, c, e) [ c >= 3 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(a, e, c, e) [ b >= a + 2 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(e, b, c, e) [ b >= a + 2 /\ c >= e^2 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c, d) -> f6(e, c, c, e) [ c >= 3 /\ c >= e^2 ] with all transitions in problem 3, the following new transitions are obtained: f0(a, b, c, d) -> f6(e', c, c, e') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 ] f0(a, b, c, d) -> f6(e, e', c, e') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ e'^2 >= c + 1 ] We thus obtain the following problem: 4: T: (1, 3) f0(a, b, c, d) -> f6(e', c, c, e') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 ] (1, 3) f0(a, b, c, d) -> f6(e, e', c, e') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ e'^2 >= c + 1 ] (1, 2) f0(a, b, c, d) -> f6(1, e, c, e) [ c >= 3 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(a, e, c, e) [ b >= a + 2 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(e, b, c, e) [ b >= a + 2 /\ c >= e^2 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c, d) -> f6(e', c, c, e') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 ] with all transitions in problem 4, the following new transitions are obtained: f0(a, b, c, d) -> f6(e'', c, c, e'') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 ] f0(a, b, c, d) -> f6(e', e'', c, e'') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ e''^2 >= c + 1 ] We thus obtain the following problem: 5: T: (1, 4) f0(a, b, c, d) -> f6(e'', c, c, e'') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 ] (1, 4) f0(a, b, c, d) -> f6(e', e'', c, e'') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ e''^2 >= c + 1 ] (1, 3) f0(a, b, c, d) -> f6(e, e', c, e') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ e'^2 >= c + 1 ] (1, 2) f0(a, b, c, d) -> f6(1, e, c, e) [ c >= 3 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(a, e, c, e) [ b >= a + 2 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(e, b, c, e) [ b >= a + 2 /\ c >= e^2 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c, d) -> f6(e'', c, c, e'') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 ] with all transitions in problem 5, the following new transitions are obtained: f0(a, b, c, d) -> f6(e''', c, c, e''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 ] f0(a, b, c, d) -> f6(e'', e''', c, e''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ e'''^2 >= c + 1 ] We thus obtain the following problem: 6: T: (1, 5) f0(a, b, c, d) -> f6(e''', c, c, e''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 ] (1, 5) f0(a, b, c, d) -> f6(e'', e''', c, e''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ e'''^2 >= c + 1 ] (1, 4) f0(a, b, c, d) -> f6(e', e'', c, e'') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ e''^2 >= c + 1 ] (1, 3) f0(a, b, c, d) -> f6(e, e', c, e') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ e'^2 >= c + 1 ] (1, 2) f0(a, b, c, d) -> f6(1, e, c, e) [ c >= 3 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(a, e, c, e) [ b >= a + 2 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(e, b, c, e) [ b >= a + 2 /\ c >= e^2 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c, d) -> f6(e''', c, c, e''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 ] with all transitions in problem 6, the following new transitions are obtained: f0(a, b, c, d) -> f6(e'''', c, c, e'''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 ] f0(a, b, c, d) -> f6(e''', e'''', c, e'''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ e''''^2 >= c + 1 ] We thus obtain the following problem: 7: T: (1, 6) f0(a, b, c, d) -> f6(e'''', c, c, e'''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 ] (1, 6) f0(a, b, c, d) -> f6(e''', e'''', c, e'''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ e''''^2 >= c + 1 ] (1, 5) f0(a, b, c, d) -> f6(e'', e''', c, e''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ e'''^2 >= c + 1 ] (1, 4) f0(a, b, c, d) -> f6(e', e'', c, e'') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ e''^2 >= c + 1 ] (1, 3) f0(a, b, c, d) -> f6(e, e', c, e') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ e'^2 >= c + 1 ] (1, 2) f0(a, b, c, d) -> f6(1, e, c, e) [ c >= 3 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(a, e, c, e) [ b >= a + 2 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(e, b, c, e) [ b >= a + 2 /\ c >= e^2 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c, d) -> f6(e'''', c, c, e'''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 ] with all transitions in problem 7, the following new transitions are obtained: f0(a, b, c, d) -> f6(e''''', c, c, e''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 ] f0(a, b, c, d) -> f6(e'''', e''''', c, e''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ e'''''^2 >= c + 1 ] We thus obtain the following problem: 8: T: (1, 7) f0(a, b, c, d) -> f6(e''''', c, c, e''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 ] (1, 7) f0(a, b, c, d) -> f6(e'''', e''''', c, e''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ e'''''^2 >= c + 1 ] (1, 6) f0(a, b, c, d) -> f6(e''', e'''', c, e'''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ e''''^2 >= c + 1 ] (1, 5) f0(a, b, c, d) -> f6(e'', e''', c, e''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ e'''^2 >= c + 1 ] (1, 4) f0(a, b, c, d) -> f6(e', e'', c, e'') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ e''^2 >= c + 1 ] (1, 3) f0(a, b, c, d) -> f6(e, e', c, e') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ e'^2 >= c + 1 ] (1, 2) f0(a, b, c, d) -> f6(1, e, c, e) [ c >= 3 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(a, e, c, e) [ b >= a + 2 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(e, b, c, e) [ b >= a + 2 /\ c >= e^2 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c, d) -> f6(e''''', c, c, e''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 ] with all transitions in problem 8, the following new transitions are obtained: f0(a, b, c, d) -> f6(e'''''', c, c, e'''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 ] f0(a, b, c, d) -> f6(e''''', e'''''', c, e'''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ e''''''^2 >= c + 1 ] We thus obtain the following problem: 9: T: (1, 8) f0(a, b, c, d) -> f6(e'''''', c, c, e'''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 ] (1, 8) f0(a, b, c, d) -> f6(e''''', e'''''', c, e'''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ e''''''^2 >= c + 1 ] (1, 7) f0(a, b, c, d) -> f6(e'''', e''''', c, e''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ e'''''^2 >= c + 1 ] (1, 6) f0(a, b, c, d) -> f6(e''', e'''', c, e'''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ e''''^2 >= c + 1 ] (1, 5) f0(a, b, c, d) -> f6(e'', e''', c, e''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ e'''^2 >= c + 1 ] (1, 4) f0(a, b, c, d) -> f6(e', e'', c, e'') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ e''^2 >= c + 1 ] (1, 3) f0(a, b, c, d) -> f6(e, e', c, e') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ e'^2 >= c + 1 ] (1, 2) f0(a, b, c, d) -> f6(1, e, c, e) [ c >= 3 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(a, e, c, e) [ b >= a + 2 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(e, b, c, e) [ b >= a + 2 /\ c >= e^2 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c, d) -> f6(e'''''', c, c, e'''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 ] with all transitions in problem 9, the following new transitions are obtained: f0(a, b, c, d) -> f6(e''''''', c, c, e''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 ] f0(a, b, c, d) -> f6(e'''''', e''''''', c, e''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ e'''''''^2 >= c + 1 ] We thus obtain the following problem: 10: T: (1, 9) f0(a, b, c, d) -> f6(e''''''', c, c, e''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 ] (1, 9) f0(a, b, c, d) -> f6(e'''''', e''''''', c, e''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ e'''''''^2 >= c + 1 ] (1, 8) f0(a, b, c, d) -> f6(e''''', e'''''', c, e'''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ e''''''^2 >= c + 1 ] (1, 7) f0(a, b, c, d) -> f6(e'''', e''''', c, e''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ e'''''^2 >= c + 1 ] (1, 6) f0(a, b, c, d) -> f6(e''', e'''', c, e'''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ e''''^2 >= c + 1 ] (1, 5) f0(a, b, c, d) -> f6(e'', e''', c, e''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ e'''^2 >= c + 1 ] (1, 4) f0(a, b, c, d) -> f6(e', e'', c, e'') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ e''^2 >= c + 1 ] (1, 3) f0(a, b, c, d) -> f6(e, e', c, e') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ e'^2 >= c + 1 ] (1, 2) f0(a, b, c, d) -> f6(1, e, c, e) [ c >= 3 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(a, e, c, e) [ b >= a + 2 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(e, b, c, e) [ b >= a + 2 /\ c >= e^2 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c, d) -> f6(e''''''', c, c, e''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 ] with all transitions in problem 10, the following new transitions are obtained: f0(a, b, c, d) -> f6(e'''''''', c, c, e'''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 ] f0(a, b, c, d) -> f6(e''''''', e'''''''', c, e'''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ e''''''''^2 >= c + 1 ] We thus obtain the following problem: 11: T: (1, 10) f0(a, b, c, d) -> f6(e'''''''', c, c, e'''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 ] (1, 10) f0(a, b, c, d) -> f6(e''''''', e'''''''', c, e'''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ e''''''''^2 >= c + 1 ] (1, 9) f0(a, b, c, d) -> f6(e'''''', e''''''', c, e''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ e'''''''^2 >= c + 1 ] (1, 8) f0(a, b, c, d) -> f6(e''''', e'''''', c, e'''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ e''''''^2 >= c + 1 ] (1, 7) f0(a, b, c, d) -> f6(e'''', e''''', c, e''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ e'''''^2 >= c + 1 ] (1, 6) f0(a, b, c, d) -> f6(e''', e'''', c, e'''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ e''''^2 >= c + 1 ] (1, 5) f0(a, b, c, d) -> f6(e'', e''', c, e''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ e'''^2 >= c + 1 ] (1, 4) f0(a, b, c, d) -> f6(e', e'', c, e'') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ e''^2 >= c + 1 ] (1, 3) f0(a, b, c, d) -> f6(e, e', c, e') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ e'^2 >= c + 1 ] (1, 2) f0(a, b, c, d) -> f6(1, e, c, e) [ c >= 3 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(a, e, c, e) [ b >= a + 2 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(e, b, c, e) [ b >= a + 2 /\ c >= e^2 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c, d) -> f6(e'''''''', c, c, e'''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 ] with all transitions in problem 11, the following new transitions are obtained: f0(a, b, c, d) -> f6(e''''''''', c, c, e''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 ] f0(a, b, c, d) -> f6(e'''''''', e''''''''', c, e''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ e'''''''''^2 >= c + 1 ] We thus obtain the following problem: 12: T: (1, 11) f0(a, b, c, d) -> f6(e''''''''', c, c, e''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 ] (1, 11) f0(a, b, c, d) -> f6(e'''''''', e''''''''', c, e''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ e'''''''''^2 >= c + 1 ] (1, 10) f0(a, b, c, d) -> f6(e''''''', e'''''''', c, e'''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ e''''''''^2 >= c + 1 ] (1, 9) f0(a, b, c, d) -> f6(e'''''', e''''''', c, e''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ e'''''''^2 >= c + 1 ] (1, 8) f0(a, b, c, d) -> f6(e''''', e'''''', c, e'''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ e''''''^2 >= c + 1 ] (1, 7) f0(a, b, c, d) -> f6(e'''', e''''', c, e''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ e'''''^2 >= c + 1 ] (1, 6) f0(a, b, c, d) -> f6(e''', e'''', c, e'''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ e''''^2 >= c + 1 ] (1, 5) f0(a, b, c, d) -> f6(e'', e''', c, e''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ e'''^2 >= c + 1 ] (1, 4) f0(a, b, c, d) -> f6(e', e'', c, e'') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ e''^2 >= c + 1 ] (1, 3) f0(a, b, c, d) -> f6(e, e', c, e') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ e'^2 >= c + 1 ] (1, 2) f0(a, b, c, d) -> f6(1, e, c, e) [ c >= 3 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(a, e, c, e) [ b >= a + 2 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(e, b, c, e) [ b >= a + 2 /\ c >= e^2 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c, d) -> f6(e''''''''', c, c, e''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 ] with all transitions in problem 12, the following new transitions are obtained: f0(a, b, c, d) -> f6(e'''''''''', c, c, e'''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 ] f0(a, b, c, d) -> f6(e''''''''', e'''''''''', c, e'''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ e''''''''''^2 >= c + 1 ] We thus obtain the following problem: 13: T: (1, 12) f0(a, b, c, d) -> f6(e'''''''''', c, c, e'''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 ] (1, 12) f0(a, b, c, d) -> f6(e''''''''', e'''''''''', c, e'''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ e''''''''''^2 >= c + 1 ] (1, 11) f0(a, b, c, d) -> f6(e'''''''', e''''''''', c, e''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ e'''''''''^2 >= c + 1 ] (1, 10) f0(a, b, c, d) -> f6(e''''''', e'''''''', c, e'''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ e''''''''^2 >= c + 1 ] (1, 9) f0(a, b, c, d) -> f6(e'''''', e''''''', c, e''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ e'''''''^2 >= c + 1 ] (1, 8) f0(a, b, c, d) -> f6(e''''', e'''''', c, e'''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ e''''''^2 >= c + 1 ] (1, 7) f0(a, b, c, d) -> f6(e'''', e''''', c, e''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ e'''''^2 >= c + 1 ] (1, 6) f0(a, b, c, d) -> f6(e''', e'''', c, e'''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ e''''^2 >= c + 1 ] (1, 5) f0(a, b, c, d) -> f6(e'', e''', c, e''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ e'''^2 >= c + 1 ] (1, 4) f0(a, b, c, d) -> f6(e', e'', c, e'') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ e''^2 >= c + 1 ] (1, 3) f0(a, b, c, d) -> f6(e, e', c, e') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ e'^2 >= c + 1 ] (1, 2) f0(a, b, c, d) -> f6(1, e, c, e) [ c >= 3 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(a, e, c, e) [ b >= a + 2 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(e, b, c, e) [ b >= a + 2 /\ c >= e^2 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c, d) -> f6(e'''''''''', c, c, e'''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 ] with all transitions in problem 13, the following new transitions are obtained: f0(a, b, c, d) -> f6(e''''''''''', c, c, e''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ c >= e'''''''''''^2 ] f0(a, b, c, d) -> f6(e'''''''''', e''''''''''', c, e''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ e'''''''''''^2 >= c + 1 ] We thus obtain the following problem: 14: T: (1, 13) f0(a, b, c, d) -> f6(e''''''''''', c, c, e''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ c >= e'''''''''''^2 ] (1, 13) f0(a, b, c, d) -> f6(e'''''''''', e''''''''''', c, e''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ e'''''''''''^2 >= c + 1 ] (1, 12) f0(a, b, c, d) -> f6(e''''''''', e'''''''''', c, e'''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ e''''''''''^2 >= c + 1 ] (1, 11) f0(a, b, c, d) -> f6(e'''''''', e''''''''', c, e''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ e'''''''''^2 >= c + 1 ] (1, 10) f0(a, b, c, d) -> f6(e''''''', e'''''''', c, e'''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ e''''''''^2 >= c + 1 ] (1, 9) f0(a, b, c, d) -> f6(e'''''', e''''''', c, e''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ e'''''''^2 >= c + 1 ] (1, 8) f0(a, b, c, d) -> f6(e''''', e'''''', c, e'''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ e''''''^2 >= c + 1 ] (1, 7) f0(a, b, c, d) -> f6(e'''', e''''', c, e''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ e'''''^2 >= c + 1 ] (1, 6) f0(a, b, c, d) -> f6(e''', e'''', c, e'''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ e''''^2 >= c + 1 ] (1, 5) f0(a, b, c, d) -> f6(e'', e''', c, e''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ e'''^2 >= c + 1 ] (1, 4) f0(a, b, c, d) -> f6(e', e'', c, e'') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ e''^2 >= c + 1 ] (1, 3) f0(a, b, c, d) -> f6(e, e', c, e') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ e'^2 >= c + 1 ] (1, 2) f0(a, b, c, d) -> f6(1, e, c, e) [ c >= 3 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(a, e, c, e) [ b >= a + 2 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(e, b, c, e) [ b >= a + 2 /\ c >= e^2 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c, d) -> f6(e''''''''''', c, c, e''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ c >= e'''''''''''^2 ] with all transitions in problem 14, the following new transitions are obtained: f0(a, b, c, d) -> f6(e'''''''''''', c, c, e'''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ c >= e'''''''''''^2 /\ c >= e''''''''''' + 2 /\ c >= e''''''''''''^2 ] f0(a, b, c, d) -> f6(e''''''''''', e'''''''''''', c, e'''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ c >= e'''''''''''^2 /\ c >= e''''''''''' + 2 /\ e''''''''''''^2 >= c + 1 ] We thus obtain the following problem: 15: T: (1, 14) f0(a, b, c, d) -> f6(e'''''''''''', c, c, e'''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ c >= e'''''''''''^2 /\ c >= e''''''''''' + 2 /\ c >= e''''''''''''^2 ] (1, 14) f0(a, b, c, d) -> f6(e''''''''''', e'''''''''''', c, e'''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ c >= e'''''''''''^2 /\ c >= e''''''''''' + 2 /\ e''''''''''''^2 >= c + 1 ] (1, 13) f0(a, b, c, d) -> f6(e'''''''''', e''''''''''', c, e''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ e'''''''''''^2 >= c + 1 ] (1, 12) f0(a, b, c, d) -> f6(e''''''''', e'''''''''', c, e'''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ e''''''''''^2 >= c + 1 ] (1, 11) f0(a, b, c, d) -> f6(e'''''''', e''''''''', c, e''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ e'''''''''^2 >= c + 1 ] (1, 10) f0(a, b, c, d) -> f6(e''''''', e'''''''', c, e'''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ e''''''''^2 >= c + 1 ] (1, 9) f0(a, b, c, d) -> f6(e'''''', e''''''', c, e''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ e'''''''^2 >= c + 1 ] (1, 8) f0(a, b, c, d) -> f6(e''''', e'''''', c, e'''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ e''''''^2 >= c + 1 ] (1, 7) f0(a, b, c, d) -> f6(e'''', e''''', c, e''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ e'''''^2 >= c + 1 ] (1, 6) f0(a, b, c, d) -> f6(e''', e'''', c, e'''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ e''''^2 >= c + 1 ] (1, 5) f0(a, b, c, d) -> f6(e'', e''', c, e''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ e'''^2 >= c + 1 ] (1, 4) f0(a, b, c, d) -> f6(e', e'', c, e'') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ e''^2 >= c + 1 ] (1, 3) f0(a, b, c, d) -> f6(e, e', c, e') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ e'^2 >= c + 1 ] (1, 2) f0(a, b, c, d) -> f6(1, e, c, e) [ c >= 3 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(a, e, c, e) [ b >= a + 2 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(e, b, c, e) [ b >= a + 2 /\ c >= e^2 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c, d) -> f6(e'''''''''''', c, c, e'''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ c >= e'''''''''''^2 /\ c >= e''''''''''' + 2 /\ c >= e''''''''''''^2 ] with all transitions in problem 15, the following new transitions are obtained: f0(a, b, c, d) -> f6(e''''''''''''', c, c, e''''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ c >= e'''''''''''^2 /\ c >= e''''''''''' + 2 /\ c >= e''''''''''''^2 /\ c >= e'''''''''''' + 2 /\ c >= e'''''''''''''^2 ] f0(a, b, c, d) -> f6(e'''''''''''', e''''''''''''', c, e''''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ c >= e'''''''''''^2 /\ c >= e''''''''''' + 2 /\ c >= e''''''''''''^2 /\ c >= e'''''''''''' + 2 /\ e'''''''''''''^2 >= c + 1 ] We thus obtain the following problem: 16: T: (1, 15) f0(a, b, c, d) -> f6(e''''''''''''', c, c, e''''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ c >= e'''''''''''^2 /\ c >= e''''''''''' + 2 /\ c >= e''''''''''''^2 /\ c >= e'''''''''''' + 2 /\ c >= e'''''''''''''^2 ] (1, 15) f0(a, b, c, d) -> f6(e'''''''''''', e''''''''''''', c, e''''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ c >= e'''''''''''^2 /\ c >= e''''''''''' + 2 /\ c >= e''''''''''''^2 /\ c >= e'''''''''''' + 2 /\ e'''''''''''''^2 >= c + 1 ] (1, 14) f0(a, b, c, d) -> f6(e''''''''''', e'''''''''''', c, e'''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ c >= e'''''''''''^2 /\ c >= e''''''''''' + 2 /\ e''''''''''''^2 >= c + 1 ] (1, 13) f0(a, b, c, d) -> f6(e'''''''''', e''''''''''', c, e''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ e'''''''''''^2 >= c + 1 ] (1, 12) f0(a, b, c, d) -> f6(e''''''''', e'''''''''', c, e'''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ e''''''''''^2 >= c + 1 ] (1, 11) f0(a, b, c, d) -> f6(e'''''''', e''''''''', c, e''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ e'''''''''^2 >= c + 1 ] (1, 10) f0(a, b, c, d) -> f6(e''''''', e'''''''', c, e'''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ e''''''''^2 >= c + 1 ] (1, 9) f0(a, b, c, d) -> f6(e'''''', e''''''', c, e''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ e'''''''^2 >= c + 1 ] (1, 8) f0(a, b, c, d) -> f6(e''''', e'''''', c, e'''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ e''''''^2 >= c + 1 ] (1, 7) f0(a, b, c, d) -> f6(e'''', e''''', c, e''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ e'''''^2 >= c + 1 ] (1, 6) f0(a, b, c, d) -> f6(e''', e'''', c, e'''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ e''''^2 >= c + 1 ] (1, 5) f0(a, b, c, d) -> f6(e'', e''', c, e''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ e'''^2 >= c + 1 ] (1, 4) f0(a, b, c, d) -> f6(e', e'', c, e'') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ e''^2 >= c + 1 ] (1, 3) f0(a, b, c, d) -> f6(e, e', c, e') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ e'^2 >= c + 1 ] (1, 2) f0(a, b, c, d) -> f6(1, e, c, e) [ c >= 3 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(a, e, c, e) [ b >= a + 2 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(e, b, c, e) [ b >= a + 2 /\ c >= e^2 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c, d) -> f6(e''''''''''''', c, c, e''''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ c >= e'''''''''''^2 /\ c >= e''''''''''' + 2 /\ c >= e''''''''''''^2 /\ c >= e'''''''''''' + 2 /\ c >= e'''''''''''''^2 ] with all transitions in problem 16, the following new transitions are obtained: f0(a, b, c, d) -> f6(e'''''''''''''', c, c, e'''''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ c >= e'''''''''''^2 /\ c >= e''''''''''' + 2 /\ c >= e''''''''''''^2 /\ c >= e'''''''''''' + 2 /\ c >= e'''''''''''''^2 /\ c >= e''''''''''''' + 2 /\ c >= e''''''''''''''^2 ] f0(a, b, c, d) -> f6(e''''''''''''', e'''''''''''''', c, e'''''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ c >= e'''''''''''^2 /\ c >= e''''''''''' + 2 /\ c >= e''''''''''''^2 /\ c >= e'''''''''''' + 2 /\ c >= e'''''''''''''^2 /\ c >= e''''''''''''' + 2 /\ e''''''''''''''^2 >= c + 1 ] We thus obtain the following problem: 17: T: (1, 16) f0(a, b, c, d) -> f6(e'''''''''''''', c, c, e'''''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ c >= e'''''''''''^2 /\ c >= e''''''''''' + 2 /\ c >= e''''''''''''^2 /\ c >= e'''''''''''' + 2 /\ c >= e'''''''''''''^2 /\ c >= e''''''''''''' + 2 /\ c >= e''''''''''''''^2 ] (1, 16) f0(a, b, c, d) -> f6(e''''''''''''', e'''''''''''''', c, e'''''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ c >= e'''''''''''^2 /\ c >= e''''''''''' + 2 /\ c >= e''''''''''''^2 /\ c >= e'''''''''''' + 2 /\ c >= e'''''''''''''^2 /\ c >= e''''''''''''' + 2 /\ e''''''''''''''^2 >= c + 1 ] (1, 15) f0(a, b, c, d) -> f6(e'''''''''''', e''''''''''''', c, e''''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ c >= e'''''''''''^2 /\ c >= e''''''''''' + 2 /\ c >= e''''''''''''^2 /\ c >= e'''''''''''' + 2 /\ e'''''''''''''^2 >= c + 1 ] (1, 14) f0(a, b, c, d) -> f6(e''''''''''', e'''''''''''', c, e'''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ c >= e'''''''''''^2 /\ c >= e''''''''''' + 2 /\ e''''''''''''^2 >= c + 1 ] (1, 13) f0(a, b, c, d) -> f6(e'''''''''', e''''''''''', c, e''''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ c >= e''''''''''^2 /\ c >= e'''''''''' + 2 /\ e'''''''''''^2 >= c + 1 ] (1, 12) f0(a, b, c, d) -> f6(e''''''''', e'''''''''', c, e'''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ c >= e'''''''''^2 /\ c >= e''''''''' + 2 /\ e''''''''''^2 >= c + 1 ] (1, 11) f0(a, b, c, d) -> f6(e'''''''', e''''''''', c, e''''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ c >= e''''''''^2 /\ c >= e'''''''' + 2 /\ e'''''''''^2 >= c + 1 ] (1, 10) f0(a, b, c, d) -> f6(e''''''', e'''''''', c, e'''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ c >= e'''''''^2 /\ c >= e''''''' + 2 /\ e''''''''^2 >= c + 1 ] (1, 9) f0(a, b, c, d) -> f6(e'''''', e''''''', c, e''''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ c >= e''''''^2 /\ c >= e'''''' + 2 /\ e'''''''^2 >= c + 1 ] (1, 8) f0(a, b, c, d) -> f6(e''''', e'''''', c, e'''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ c >= e'''''^2 /\ c >= e''''' + 2 /\ e''''''^2 >= c + 1 ] (1, 7) f0(a, b, c, d) -> f6(e'''', e''''', c, e''''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ c >= e''''^2 /\ c >= e'''' + 2 /\ e'''''^2 >= c + 1 ] (1, 6) f0(a, b, c, d) -> f6(e''', e'''', c, e'''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ c >= e'''^2 /\ c >= e''' + 2 /\ e''''^2 >= c + 1 ] (1, 5) f0(a, b, c, d) -> f6(e'', e''', c, e''') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ c >= e''^2 /\ c >= e'' + 2 /\ e'''^2 >= c + 1 ] (1, 4) f0(a, b, c, d) -> f6(e', e'', c, e'') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ c >= e'^2 /\ c >= e' + 2 /\ e''^2 >= c + 1 ] (1, 3) f0(a, b, c, d) -> f6(e, e', c, e') [ c >= 3 /\ c >= e^2 /\ c >= e + 2 /\ e'^2 >= c + 1 ] (1, 2) f0(a, b, c, d) -> f6(1, e, c, e) [ c >= 3 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(a, e, c, e) [ b >= a + 2 /\ e^2 >= c + 1 ] (?, 1) f6(a, b, c, d) -> f6(e, b, c, e) [ b >= a + 2 /\ c >= e^2 ] start location: f0 leaf cost: 1 Complexity upper bound ? Time: 1.539 sec (SMT: 1.340 sec)