MAYBE

Initial complexity problem:
1:	T:
		(?, 1)    f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> f1(a, b + 1, d, q, d, r, b, h, i, j, k, l, m, n, o, p) [ a >= b + 1 /\ b >= 0 ]
		(?, 1)    f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> f4(r, s, u, x, w, f, g, q, t, v, y, z, c, n, o, p) [ b >= a /\ b >= 0 /\ s >= q /\ q >= 2 ]
		(1, 1)    f3(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> f4(t, v, s, y, x, f, g, r, u, w, z, b1, o, q, o, p) [ 0 >= r /\ 0 >= a1 ]
		(1, 1)    f3(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> f1(r, 2, u, s, u, f, g, r, t, u, k, l, m, q, t, v) [ r >= 2 ]
		(1, 1)    f3(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -> f4(r, s, u, y, x, f, g, 1, t, w, z, b1, d, q, v, p)
	start location:	f3
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b].
We thus obtain the following problem:
2:	T:
		(1, 1)    f3(a, b) -> f4(r, s)
		(1, 1)    f3(a, b) -> f1(r, 2) [ r >= 2 ]
		(1, 1)    f3(a, b) -> f4(t, v) [ 0 >= r /\ 0 >= a1 ]
		(?, 1)    f1(a, b) -> f4(r, s) [ b >= a /\ b >= 0 /\ s >= q /\ q >= 2 ]
		(?, 1)    f1(a, b) -> f1(a, b + 1) [ a >= b + 1 /\ b >= 0 ]
	start location:	f3
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem:
3:	T:
		(1, 1)    f3(a, b) -> f1(r, 2) [ r >= 2 ]
		(?, 1)    f1(a, b) -> f1(a, b + 1) [ a >= b + 1 /\ b >= 0 ]
	start location:	f3
	leaf cost:	3

Applied AI with 'oct' on problem 3 to obtain the following invariants:
  For symbol f1: X_1 - X_2 >= 0 /\ X_2 - 2 >= 0 /\ X_1 + X_2 - 4 >= 0 /\ X_1 - 2 >= 0


This yielded the following problem:
4:	T:
		(?, 1)    f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ]
		(1, 1)    f3(a, b) -> f1(r, 2) [ r >= 2 ]
	start location:	f3
	leaf cost:	3

By chaining the transition f3(a, b) -> f1(r, 2) [ r >= 2 ] with all transitions in problem 4, the following new transition is obtained:
	f3(a, b) -> f1(r, 3) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 ]
We thus obtain the following problem:
5:	T:
		(1, 2)    f3(a, b) -> f1(r, 3) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 ]
		(?, 1)    f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ]
	start location:	f3
	leaf cost:	3

By chaining the transition f3(a, b) -> f1(r, 3) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 ] with all transitions in problem 5, the following new transition is obtained:
	f3(a, b) -> f1(r, 4) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 ]
We thus obtain the following problem:
6:	T:
		(1, 3)    f3(a, b) -> f1(r, 4) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 ]
		(?, 1)    f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ]
	start location:	f3
	leaf cost:	3

By chaining the transition f3(a, b) -> f1(r, 4) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 ] with all transitions in problem 6, the following new transition is obtained:
	f3(a, b) -> f1(r, 5) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 ]
We thus obtain the following problem:
7:	T:
		(1, 4)    f3(a, b) -> f1(r, 5) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 ]
		(?, 1)    f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ]
	start location:	f3
	leaf cost:	3

By chaining the transition f3(a, b) -> f1(r, 5) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 ] with all transitions in problem 7, the following new transition is obtained:
	f3(a, b) -> f1(r, 6) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 ]
We thus obtain the following problem:
8:	T:
		(1, 5)    f3(a, b) -> f1(r, 6) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 ]
		(?, 1)    f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ]
	start location:	f3
	leaf cost:	3

By chaining the transition f3(a, b) -> f1(r, 6) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 ] with all transitions in problem 8, the following new transition is obtained:
	f3(a, b) -> f1(r, 7) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 ]
We thus obtain the following problem:
9:	T:
		(1, 6)    f3(a, b) -> f1(r, 7) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 ]
		(?, 1)    f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ]
	start location:	f3
	leaf cost:	3

By chaining the transition f3(a, b) -> f1(r, 7) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 ] with all transitions in problem 9, the following new transition is obtained:
	f3(a, b) -> f1(r, 8) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 ]
We thus obtain the following problem:
10:	T:
		(1, 7)    f3(a, b) -> f1(r, 8) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 ]
		(?, 1)    f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ]
	start location:	f3
	leaf cost:	3

By chaining the transition f3(a, b) -> f1(r, 8) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 ] with all transitions in problem 10, the following new transition is obtained:
	f3(a, b) -> f1(r, 9) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 ]
We thus obtain the following problem:
11:	T:
		(1, 8)    f3(a, b) -> f1(r, 9) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 ]
		(?, 1)    f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ]
	start location:	f3
	leaf cost:	3

By chaining the transition f3(a, b) -> f1(r, 9) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 ] with all transitions in problem 11, the following new transition is obtained:
	f3(a, b) -> f1(r, 10) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 /\ r - 9 >= 0 /\ r + 5 >= 0 /\ r >= 10 /\ 9 >= 0 ]
We thus obtain the following problem:
12:	T:
		(1, 9)    f3(a, b) -> f1(r, 10) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 /\ r - 9 >= 0 /\ r + 5 >= 0 /\ r >= 10 /\ 9 >= 0 ]
		(?, 1)    f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ]
	start location:	f3
	leaf cost:	3

By chaining the transition f3(a, b) -> f1(r, 10) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 /\ r - 9 >= 0 /\ r + 5 >= 0 /\ r >= 10 /\ 9 >= 0 ] with all transitions in problem 12, the following new transition is obtained:
	f3(a, b) -> f1(r, 11) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 /\ r - 9 >= 0 /\ r + 5 >= 0 /\ r >= 10 /\ 9 >= 0 /\ r - 10 >= 0 /\ r + 6 >= 0 /\ r >= 11 /\ 10 >= 0 ]
We thus obtain the following problem:
13:	T:
		(1, 10)    f3(a, b) -> f1(r, 11) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 /\ r - 9 >= 0 /\ r + 5 >= 0 /\ r >= 10 /\ 9 >= 0 /\ r - 10 >= 0 /\ r + 6 >= 0 /\ r >= 11 /\ 10 >= 0 ]
		(?, 1)     f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ]
	start location:	f3
	leaf cost:	3

By chaining the transition f3(a, b) -> f1(r, 11) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 /\ r - 9 >= 0 /\ r + 5 >= 0 /\ r >= 10 /\ 9 >= 0 /\ r - 10 >= 0 /\ r + 6 >= 0 /\ r >= 11 /\ 10 >= 0 ] with all transitions in problem 13, the following new transition is obtained:
	f3(a, b) -> f1(r, 12) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 /\ r - 9 >= 0 /\ r + 5 >= 0 /\ r >= 10 /\ 9 >= 0 /\ r - 10 >= 0 /\ r + 6 >= 0 /\ r >= 11 /\ 10 >= 0 /\ r - 11 >= 0 /\ r + 7 >= 0 /\ r >= 12 /\ 11 >= 0 ]
We thus obtain the following problem:
14:	T:
		(1, 11)    f3(a, b) -> f1(r, 12) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 /\ r - 9 >= 0 /\ r + 5 >= 0 /\ r >= 10 /\ 9 >= 0 /\ r - 10 >= 0 /\ r + 6 >= 0 /\ r >= 11 /\ 10 >= 0 /\ r - 11 >= 0 /\ r + 7 >= 0 /\ r >= 12 /\ 11 >= 0 ]
		(?, 1)     f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ]
	start location:	f3
	leaf cost:	3

By chaining the transition f3(a, b) -> f1(r, 12) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 /\ r - 9 >= 0 /\ r + 5 >= 0 /\ r >= 10 /\ 9 >= 0 /\ r - 10 >= 0 /\ r + 6 >= 0 /\ r >= 11 /\ 10 >= 0 /\ r - 11 >= 0 /\ r + 7 >= 0 /\ r >= 12 /\ 11 >= 0 ] with all transitions in problem 14, the following new transition is obtained:
	f3(a, b) -> f1(r, 13) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 /\ r - 9 >= 0 /\ r + 5 >= 0 /\ r >= 10 /\ 9 >= 0 /\ r - 10 >= 0 /\ r + 6 >= 0 /\ r >= 11 /\ 10 >= 0 /\ r - 11 >= 0 /\ r + 7 >= 0 /\ r >= 12 /\ 11 >= 0 /\ r - 12 >= 0 /\ r + 8 >= 0 /\ r >= 13 /\ 12 >= 0 ]
We thus obtain the following problem:
15:	T:
		(1, 12)    f3(a, b) -> f1(r, 13) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 /\ r - 9 >= 0 /\ r + 5 >= 0 /\ r >= 10 /\ 9 >= 0 /\ r - 10 >= 0 /\ r + 6 >= 0 /\ r >= 11 /\ 10 >= 0 /\ r - 11 >= 0 /\ r + 7 >= 0 /\ r >= 12 /\ 11 >= 0 /\ r - 12 >= 0 /\ r + 8 >= 0 /\ r >= 13 /\ 12 >= 0 ]
		(?, 1)     f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ]
	start location:	f3
	leaf cost:	3

By chaining the transition f3(a, b) -> f1(r, 13) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 /\ r - 9 >= 0 /\ r + 5 >= 0 /\ r >= 10 /\ 9 >= 0 /\ r - 10 >= 0 /\ r + 6 >= 0 /\ r >= 11 /\ 10 >= 0 /\ r - 11 >= 0 /\ r + 7 >= 0 /\ r >= 12 /\ 11 >= 0 /\ r - 12 >= 0 /\ r + 8 >= 0 /\ r >= 13 /\ 12 >= 0 ] with all transitions in problem 15, the following new transition is obtained:
	f3(a, b) -> f1(r, 14) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 /\ r - 9 >= 0 /\ r + 5 >= 0 /\ r >= 10 /\ 9 >= 0 /\ r - 10 >= 0 /\ r + 6 >= 0 /\ r >= 11 /\ 10 >= 0 /\ r - 11 >= 0 /\ r + 7 >= 0 /\ r >= 12 /\ 11 >= 0 /\ r - 12 >= 0 /\ r + 8 >= 0 /\ r >= 13 /\ 12 >= 0 /\ r - 13 >= 0 /\ r + 9 >= 0 /\ r >= 14 /\ 13 >= 0 ]
We thus obtain the following problem:
16:	T:
		(1, 13)    f3(a, b) -> f1(r, 14) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 /\ r - 9 >= 0 /\ r + 5 >= 0 /\ r >= 10 /\ 9 >= 0 /\ r - 10 >= 0 /\ r + 6 >= 0 /\ r >= 11 /\ 10 >= 0 /\ r - 11 >= 0 /\ r + 7 >= 0 /\ r >= 12 /\ 11 >= 0 /\ r - 12 >= 0 /\ r + 8 >= 0 /\ r >= 13 /\ 12 >= 0 /\ r - 13 >= 0 /\ r + 9 >= 0 /\ r >= 14 /\ 13 >= 0 ]
		(?, 1)     f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ]
	start location:	f3
	leaf cost:	3

By chaining the transition f3(a, b) -> f1(r, 14) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 /\ r - 9 >= 0 /\ r + 5 >= 0 /\ r >= 10 /\ 9 >= 0 /\ r - 10 >= 0 /\ r + 6 >= 0 /\ r >= 11 /\ 10 >= 0 /\ r - 11 >= 0 /\ r + 7 >= 0 /\ r >= 12 /\ 11 >= 0 /\ r - 12 >= 0 /\ r + 8 >= 0 /\ r >= 13 /\ 12 >= 0 /\ r - 13 >= 0 /\ r + 9 >= 0 /\ r >= 14 /\ 13 >= 0 ] with all transitions in problem 16, the following new transition is obtained:
	f3(a, b) -> f1(r, 15) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 /\ r - 9 >= 0 /\ r + 5 >= 0 /\ r >= 10 /\ 9 >= 0 /\ r - 10 >= 0 /\ r + 6 >= 0 /\ r >= 11 /\ 10 >= 0 /\ r - 11 >= 0 /\ r + 7 >= 0 /\ r >= 12 /\ 11 >= 0 /\ r - 12 >= 0 /\ r + 8 >= 0 /\ r >= 13 /\ 12 >= 0 /\ r - 13 >= 0 /\ r + 9 >= 0 /\ r >= 14 /\ 13 >= 0 /\ r - 14 >= 0 /\ r + 10 >= 0 /\ r >= 15 /\ 14 >= 0 ]
We thus obtain the following problem:
17:	T:
		(1, 14)    f3(a, b) -> f1(r, 15) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 /\ r - 9 >= 0 /\ r + 5 >= 0 /\ r >= 10 /\ 9 >= 0 /\ r - 10 >= 0 /\ r + 6 >= 0 /\ r >= 11 /\ 10 >= 0 /\ r - 11 >= 0 /\ r + 7 >= 0 /\ r >= 12 /\ 11 >= 0 /\ r - 12 >= 0 /\ r + 8 >= 0 /\ r >= 13 /\ 12 >= 0 /\ r - 13 >= 0 /\ r + 9 >= 0 /\ r >= 14 /\ 13 >= 0 /\ r - 14 >= 0 /\ r + 10 >= 0 /\ r >= 15 /\ 14 >= 0 ]
		(?, 1)     f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ]
	start location:	f3
	leaf cost:	3

By chaining the transition f3(a, b) -> f1(r, 15) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 /\ r - 9 >= 0 /\ r + 5 >= 0 /\ r >= 10 /\ 9 >= 0 /\ r - 10 >= 0 /\ r + 6 >= 0 /\ r >= 11 /\ 10 >= 0 /\ r - 11 >= 0 /\ r + 7 >= 0 /\ r >= 12 /\ 11 >= 0 /\ r - 12 >= 0 /\ r + 8 >= 0 /\ r >= 13 /\ 12 >= 0 /\ r - 13 >= 0 /\ r + 9 >= 0 /\ r >= 14 /\ 13 >= 0 /\ r - 14 >= 0 /\ r + 10 >= 0 /\ r >= 15 /\ 14 >= 0 ] with all transitions in problem 17, the following new transition is obtained:
	f3(a, b) -> f1(r, 16) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 /\ r - 9 >= 0 /\ r + 5 >= 0 /\ r >= 10 /\ 9 >= 0 /\ r - 10 >= 0 /\ r + 6 >= 0 /\ r >= 11 /\ 10 >= 0 /\ r - 11 >= 0 /\ r + 7 >= 0 /\ r >= 12 /\ 11 >= 0 /\ r - 12 >= 0 /\ r + 8 >= 0 /\ r >= 13 /\ 12 >= 0 /\ r - 13 >= 0 /\ r + 9 >= 0 /\ r >= 14 /\ 13 >= 0 /\ r - 14 >= 0 /\ r + 10 >= 0 /\ r >= 15 /\ 14 >= 0 /\ r - 15 >= 0 /\ r + 11 >= 0 /\ r >= 16 /\ 15 >= 0 ]
We thus obtain the following problem:
18:	T:
		(1, 15)    f3(a, b) -> f1(r, 16) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 /\ r - 9 >= 0 /\ r + 5 >= 0 /\ r >= 10 /\ 9 >= 0 /\ r - 10 >= 0 /\ r + 6 >= 0 /\ r >= 11 /\ 10 >= 0 /\ r - 11 >= 0 /\ r + 7 >= 0 /\ r >= 12 /\ 11 >= 0 /\ r - 12 >= 0 /\ r + 8 >= 0 /\ r >= 13 /\ 12 >= 0 /\ r - 13 >= 0 /\ r + 9 >= 0 /\ r >= 14 /\ 13 >= 0 /\ r - 14 >= 0 /\ r + 10 >= 0 /\ r >= 15 /\ 14 >= 0 /\ r - 15 >= 0 /\ r + 11 >= 0 /\ r >= 16 /\ 15 >= 0 ]
		(?, 1)     f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ]
	start location:	f3
	leaf cost:	3

By chaining the transition f3(a, b) -> f1(r, 16) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 /\ r - 9 >= 0 /\ r + 5 >= 0 /\ r >= 10 /\ 9 >= 0 /\ r - 10 >= 0 /\ r + 6 >= 0 /\ r >= 11 /\ 10 >= 0 /\ r - 11 >= 0 /\ r + 7 >= 0 /\ r >= 12 /\ 11 >= 0 /\ r - 12 >= 0 /\ r + 8 >= 0 /\ r >= 13 /\ 12 >= 0 /\ r - 13 >= 0 /\ r + 9 >= 0 /\ r >= 14 /\ 13 >= 0 /\ r - 14 >= 0 /\ r + 10 >= 0 /\ r >= 15 /\ 14 >= 0 /\ r - 15 >= 0 /\ r + 11 >= 0 /\ r >= 16 /\ 15 >= 0 ] with all transitions in problem 18, the following new transition is obtained:
	f3(a, b) -> f1(r, 17) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 /\ r - 9 >= 0 /\ r + 5 >= 0 /\ r >= 10 /\ 9 >= 0 /\ r - 10 >= 0 /\ r + 6 >= 0 /\ r >= 11 /\ 10 >= 0 /\ r - 11 >= 0 /\ r + 7 >= 0 /\ r >= 12 /\ 11 >= 0 /\ r - 12 >= 0 /\ r + 8 >= 0 /\ r >= 13 /\ 12 >= 0 /\ r - 13 >= 0 /\ r + 9 >= 0 /\ r >= 14 /\ 13 >= 0 /\ r - 14 >= 0 /\ r + 10 >= 0 /\ r >= 15 /\ 14 >= 0 /\ r - 15 >= 0 /\ r + 11 >= 0 /\ r >= 16 /\ 15 >= 0 /\ r - 16 >= 0 /\ r + 12 >= 0 /\ r >= 17 /\ 16 >= 0 ]
We thus obtain the following problem:
19:	T:
		(1, 16)    f3(a, b) -> f1(r, 17) [ r >= 2 /\ r - 2 >= 0 /\ 0 >= 0 /\ r >= 3 /\ 2 >= 0 /\ r - 3 >= 0 /\ 1 >= 0 /\ r - 1 >= 0 /\ r >= 4 /\ 3 >= 0 /\ r - 4 >= 0 /\ r >= 0 /\ r >= 5 /\ 4 >= 0 /\ r - 5 >= 0 /\ r + 1 >= 0 /\ r >= 6 /\ 5 >= 0 /\ r - 6 >= 0 /\ r + 2 >= 0 /\ r >= 7 /\ 6 >= 0 /\ r - 7 >= 0 /\ r + 3 >= 0 /\ r >= 8 /\ 7 >= 0 /\ r - 8 >= 0 /\ r + 4 >= 0 /\ r >= 9 /\ 8 >= 0 /\ r - 9 >= 0 /\ r + 5 >= 0 /\ r >= 10 /\ 9 >= 0 /\ r - 10 >= 0 /\ r + 6 >= 0 /\ r >= 11 /\ 10 >= 0 /\ r - 11 >= 0 /\ r + 7 >= 0 /\ r >= 12 /\ 11 >= 0 /\ r - 12 >= 0 /\ r + 8 >= 0 /\ r >= 13 /\ 12 >= 0 /\ r - 13 >= 0 /\ r + 9 >= 0 /\ r >= 14 /\ 13 >= 0 /\ r - 14 >= 0 /\ r + 10 >= 0 /\ r >= 15 /\ 14 >= 0 /\ r - 15 >= 0 /\ r + 11 >= 0 /\ r >= 16 /\ 15 >= 0 /\ r - 16 >= 0 /\ r + 12 >= 0 /\ r >= 17 /\ 16 >= 0 ]
		(?, 1)     f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ]
	start location:	f3
	leaf cost:	3

Complexity upper bound ?

Time: 0.869 sec (SMT: 0.758 sec)