MAYBE

Initial complexity problem:
1:	T:
		(1, 1)    evalgcdstart(a, b) -> evalgcdentryin(a, b)
		(?, 1)    evalgcdentryin(a, b) -> evalgcdreturnin(a, b) [ 0 >= a ]
		(?, 1)    evalgcdentryin(a, b) -> evalgcdreturnin(a, b) [ 0 >= b ]
		(?, 1)    evalgcdentryin(a, b) -> evalgcdbb7in(b, a) [ a >= 1 /\ b >= 1 ]
		(?, 1)    evalgcdbb7in(a, b) -> evalgcdbb4in(a, b) [ a >= b + 1 ]
		(?, 1)    evalgcdbb7in(a, b) -> evalgcdbb4in(a, b) [ b >= a + 1 ]
		(?, 1)    evalgcdbb7in(a, b) -> evalgcdreturnin(a, b) [ b = a ]
		(?, 1)    evalgcdbb4in(a, b) -> evalgcdbb5in(a, b) [ a >= b + 1 ]
		(?, 1)    evalgcdbb4in(a, b) -> evalgcdbb6in(a, b) [ b >= a ]
		(?, 1)    evalgcdbb5in(a, b) -> evalgcdbb7in(a - b, b)
		(?, 1)    evalgcdbb6in(a, b) -> evalgcdbb7in(a, b - a)
		(?, 1)    evalgcdreturnin(a, b) -> evalgcdstop(a, b)
	start location:	evalgcdstart
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalgcdstart(a, b) -> evalgcdentryin(a, b)
		(?, 1)    evalgcdentryin(a, b) -> evalgcdbb7in(b, a) [ a >= 1 /\ b >= 1 ]
		(?, 1)    evalgcdbb7in(a, b) -> evalgcdbb4in(a, b) [ a >= b + 1 ]
		(?, 1)    evalgcdbb7in(a, b) -> evalgcdbb4in(a, b) [ b >= a + 1 ]
		(?, 1)    evalgcdbb4in(a, b) -> evalgcdbb5in(a, b) [ a >= b + 1 ]
		(?, 1)    evalgcdbb4in(a, b) -> evalgcdbb6in(a, b) [ b >= a ]
		(?, 1)    evalgcdbb5in(a, b) -> evalgcdbb7in(a - b, b)
		(?, 1)    evalgcdbb6in(a, b) -> evalgcdbb7in(a, b - a)
	start location:	evalgcdstart
	leaf cost:	4

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalgcdstart(a, b) -> evalgcdentryin(a, b)
		(1, 1)    evalgcdentryin(a, b) -> evalgcdbb7in(b, a) [ a >= 1 /\ b >= 1 ]
		(?, 1)    evalgcdbb7in(a, b) -> evalgcdbb4in(a, b) [ a >= b + 1 ]
		(?, 1)    evalgcdbb7in(a, b) -> evalgcdbb4in(a, b) [ b >= a + 1 ]
		(?, 1)    evalgcdbb4in(a, b) -> evalgcdbb5in(a, b) [ a >= b + 1 ]
		(?, 1)    evalgcdbb4in(a, b) -> evalgcdbb6in(a, b) [ b >= a ]
		(?, 1)    evalgcdbb5in(a, b) -> evalgcdbb7in(a - b, b)
		(?, 1)    evalgcdbb6in(a, b) -> evalgcdbb7in(a, b - a)
	start location:	evalgcdstart
	leaf cost:	4

Applied AI with 'oct' on problem 3 to obtain the following invariants:
  For symbol evalgcdbb5in: X_1 - X_2 - 1 >= 0
  For symbol evalgcdbb6in: -X_1 + X_2 >= 0


This yielded the following problem:
4:	T:
		(?, 1)    evalgcdbb6in(a, b) -> evalgcdbb7in(a, b - a) [ -a + b >= 0 ]
		(?, 1)    evalgcdbb5in(a, b) -> evalgcdbb7in(a - b, b) [ a - b - 1 >= 0 ]
		(?, 1)    evalgcdbb4in(a, b) -> evalgcdbb6in(a, b) [ b >= a ]
		(?, 1)    evalgcdbb4in(a, b) -> evalgcdbb5in(a, b) [ a >= b + 1 ]
		(?, 1)    evalgcdbb7in(a, b) -> evalgcdbb4in(a, b) [ b >= a + 1 ]
		(?, 1)    evalgcdbb7in(a, b) -> evalgcdbb4in(a, b) [ a >= b + 1 ]
		(1, 1)    evalgcdentryin(a, b) -> evalgcdbb7in(b, a) [ a >= 1 /\ b >= 1 ]
		(1, 1)    evalgcdstart(a, b) -> evalgcdentryin(a, b)
	start location:	evalgcdstart
	leaf cost:	4

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

Testing for reachability in the complexity graph removes the following transition from problem 5:
	evalgcdbb6in(a, b) -> evalgcdbb7in(a, b - a) [ -a + b >= 0 ]
We thus obtain the following problem:
6:	T:
		(?, 1)    evalgcdbb5in(a, b) -> evalgcdbb7in(a - b, b) [ a - b - 1 >= 0 ]
		(?, 1)    evalgcdbb4in(a, b) -> evalgcdbb5in(a, b) [ a >= b + 1 ]
		(?, 2)    evalgcdbb4in(a, b) -> evalgcdbb7in(a, b - a) [ b >= a /\ -a + b >= 0 ]
		(?, 1)    evalgcdbb7in(a, b) -> evalgcdbb4in(a, b) [ a >= b + 1 ]
		(?, 1)    evalgcdbb7in(a, b) -> evalgcdbb4in(a, b) [ b >= a + 1 ]
		(1, 1)    evalgcdentryin(a, b) -> evalgcdbb7in(b, a) [ a >= 1 /\ b >= 1 ]
		(1, 1)    evalgcdstart(a, b) -> evalgcdentryin(a, b)
	start location:	evalgcdstart
	leaf cost:	4

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

Testing for reachability in the complexity graph removes the following transition from problem 7:
	evalgcdbb5in(a, b) -> evalgcdbb7in(a - b, b) [ a - b - 1 >= 0 ]
We thus obtain the following problem:
8:	T:
		(?, 2)    evalgcdbb4in(a, b) -> evalgcdbb7in(a - b, b) [ a >= b + 1 /\ a - b - 1 >= 0 ]
		(?, 2)    evalgcdbb4in(a, b) -> evalgcdbb7in(a, b - a) [ b >= a /\ -a + b >= 0 ]
		(?, 1)    evalgcdbb7in(a, b) -> evalgcdbb4in(a, b) [ a >= b + 1 ]
		(?, 1)    evalgcdbb7in(a, b) -> evalgcdbb4in(a, b) [ b >= a + 1 ]
		(1, 1)    evalgcdentryin(a, b) -> evalgcdbb7in(b, a) [ a >= 1 /\ b >= 1 ]
		(1, 1)    evalgcdstart(a, b) -> evalgcdentryin(a, b)
	start location:	evalgcdstart
	leaf cost:	4

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

Testing for reachability in the complexity graph removes the following transition from problem 9:
	evalgcdbb4in(a, b) -> evalgcdbb7in(a - b, b) [ a >= b + 1 /\ a - b - 1 >= 0 ]
We thus obtain the following problem:
10:	T:
		(?, 2)    evalgcdbb4in(a, b) -> evalgcdbb7in(a, b - a) [ b >= a /\ -a + b >= 0 ]
		(?, 3)    evalgcdbb7in(a, b) -> evalgcdbb7in(a - b, b) [ a >= b + 1 /\ a - b - 1 >= 0 ]
		(?, 1)    evalgcdbb7in(a, b) -> evalgcdbb4in(a, b) [ b >= a + 1 ]
		(1, 1)    evalgcdentryin(a, b) -> evalgcdbb7in(b, a) [ a >= 1 /\ b >= 1 ]
		(1, 1)    evalgcdstart(a, b) -> evalgcdentryin(a, b)
	start location:	evalgcdstart
	leaf cost:	4

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

Testing for reachability in the complexity graph removes the following transition from problem 11:
	evalgcdbb4in(a, b) -> evalgcdbb7in(a, b - a) [ b >= a /\ -a + b >= 0 ]
We thus obtain the following problem:
12:	T:
		(?, 3)    evalgcdbb7in(a, b) -> evalgcdbb7in(a, b - a) [ b >= a + 1 /\ b >= a /\ -a + b >= 0 ]
		(?, 3)    evalgcdbb7in(a, b) -> evalgcdbb7in(a - b, b) [ a >= b + 1 /\ a - b - 1 >= 0 ]
		(1, 1)    evalgcdentryin(a, b) -> evalgcdbb7in(b, a) [ a >= 1 /\ b >= 1 ]
		(1, 1)    evalgcdstart(a, b) -> evalgcdentryin(a, b)
	start location:	evalgcdstart
	leaf cost:	4

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

Testing for reachability in the complexity graph removes the following transition from problem 13:
	evalgcdentryin(a, b) -> evalgcdbb7in(b, a) [ a >= 1 /\ b >= 1 ]
We thus obtain the following problem:
14:	T:
		(?, 3)    evalgcdbb7in(a, b) -> evalgcdbb7in(a, b - a) [ b >= a + 1 /\ b >= a /\ -a + b >= 0 ]
		(?, 3)    evalgcdbb7in(a, b) -> evalgcdbb7in(a - b, b) [ a >= b + 1 /\ a - b - 1 >= 0 ]
		(1, 2)    evalgcdstart(a, b) -> evalgcdbb7in(b, a) [ a >= 1 /\ b >= 1 ]
	start location:	evalgcdstart
	leaf cost:	4

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

By chaining the transition evalgcdstart(a, b) -> evalgcdbb7in(b, a - b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 ] with all transitions in problem 15, the following new transitions are obtained:
	evalgcdstart(a, b) -> evalgcdbb7in(b, a - 2*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 ]
	evalgcdstart(a, b) -> evalgcdbb7in(2*b - a, a - b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ b >= a - b + 1 /\ 2*b - a - 1 >= 0 ]
We thus obtain the following problem:
16:	T:
		(1, 8)    evalgcdstart(a, b) -> evalgcdbb7in(b, a - 2*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 ]
		(1, 8)    evalgcdstart(a, b) -> evalgcdbb7in(2*b - a, a - b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ b >= a - b + 1 /\ 2*b - a - 1 >= 0 ]
		(1, 5)    evalgcdstart(a, b) -> evalgcdbb7in(b - a, a) [ a >= 1 /\ b >= 1 /\ b >= a + 1 /\ b - a - 1 >= 0 ]
		(?, 3)    evalgcdbb7in(a, b) -> evalgcdbb7in(a, b - a) [ b >= a + 1 /\ b >= a /\ -a + b >= 0 ]
		(?, 3)    evalgcdbb7in(a, b) -> evalgcdbb7in(a - b, b) [ a >= b + 1 /\ a - b - 1 >= 0 ]
	start location:	evalgcdstart
	leaf cost:	4

By chaining the transition evalgcdstart(a, b) -> evalgcdbb7in(b, a - 2*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 ] with all transitions in problem 16, the following new transitions are obtained:
	evalgcdstart(a, b) -> evalgcdbb7in(b, a - 3*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 ]
	evalgcdstart(a, b) -> evalgcdbb7in(3*b - a, a - 2*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ b >= a - 2*b + 1 /\ 3*b - a - 1 >= 0 ]
We thus obtain the following problem:
17:	T:
		(1, 11)    evalgcdstart(a, b) -> evalgcdbb7in(b, a - 3*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 ]
		(1, 11)    evalgcdstart(a, b) -> evalgcdbb7in(3*b - a, a - 2*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ b >= a - 2*b + 1 /\ 3*b - a - 1 >= 0 ]
		(1, 8)     evalgcdstart(a, b) -> evalgcdbb7in(2*b - a, a - b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ b >= a - b + 1 /\ 2*b - a - 1 >= 0 ]
		(1, 5)     evalgcdstart(a, b) -> evalgcdbb7in(b - a, a) [ a >= 1 /\ b >= 1 /\ b >= a + 1 /\ b - a - 1 >= 0 ]
		(?, 3)     evalgcdbb7in(a, b) -> evalgcdbb7in(a, b - a) [ b >= a + 1 /\ b >= a /\ -a + b >= 0 ]
		(?, 3)     evalgcdbb7in(a, b) -> evalgcdbb7in(a - b, b) [ a >= b + 1 /\ a - b - 1 >= 0 ]
	start location:	evalgcdstart
	leaf cost:	4

By chaining the transition evalgcdstart(a, b) -> evalgcdbb7in(b, a - 3*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 ] with all transitions in problem 17, the following new transitions are obtained:
	evalgcdstart(a, b) -> evalgcdbb7in(b, a - 4*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 ]
	evalgcdstart(a, b) -> evalgcdbb7in(4*b - a, a - 3*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ b >= a - 3*b + 1 /\ 4*b - a - 1 >= 0 ]
We thus obtain the following problem:
18:	T:
		(1, 14)    evalgcdstart(a, b) -> evalgcdbb7in(b, a - 4*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 ]
		(1, 14)    evalgcdstart(a, b) -> evalgcdbb7in(4*b - a, a - 3*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ b >= a - 3*b + 1 /\ 4*b - a - 1 >= 0 ]
		(1, 11)    evalgcdstart(a, b) -> evalgcdbb7in(3*b - a, a - 2*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ b >= a - 2*b + 1 /\ 3*b - a - 1 >= 0 ]
		(1, 8)     evalgcdstart(a, b) -> evalgcdbb7in(2*b - a, a - b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ b >= a - b + 1 /\ 2*b - a - 1 >= 0 ]
		(1, 5)     evalgcdstart(a, b) -> evalgcdbb7in(b - a, a) [ a >= 1 /\ b >= 1 /\ b >= a + 1 /\ b - a - 1 >= 0 ]
		(?, 3)     evalgcdbb7in(a, b) -> evalgcdbb7in(a, b - a) [ b >= a + 1 /\ b >= a /\ -a + b >= 0 ]
		(?, 3)     evalgcdbb7in(a, b) -> evalgcdbb7in(a - b, b) [ a >= b + 1 /\ a - b - 1 >= 0 ]
	start location:	evalgcdstart
	leaf cost:	4

By chaining the transition evalgcdstart(a, b) -> evalgcdbb7in(b, a - 4*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 ] with all transitions in problem 18, the following new transitions are obtained:
	evalgcdstart(a, b) -> evalgcdbb7in(b, a - 5*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 ]
	evalgcdstart(a, b) -> evalgcdbb7in(5*b - a, a - 4*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ b >= a - 4*b + 1 /\ 5*b - a - 1 >= 0 ]
We thus obtain the following problem:
19:	T:
		(1, 17)    evalgcdstart(a, b) -> evalgcdbb7in(b, a - 5*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 ]
		(1, 17)    evalgcdstart(a, b) -> evalgcdbb7in(5*b - a, a - 4*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ b >= a - 4*b + 1 /\ 5*b - a - 1 >= 0 ]
		(1, 14)    evalgcdstart(a, b) -> evalgcdbb7in(4*b - a, a - 3*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ b >= a - 3*b + 1 /\ 4*b - a - 1 >= 0 ]
		(1, 11)    evalgcdstart(a, b) -> evalgcdbb7in(3*b - a, a - 2*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ b >= a - 2*b + 1 /\ 3*b - a - 1 >= 0 ]
		(1, 8)     evalgcdstart(a, b) -> evalgcdbb7in(2*b - a, a - b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ b >= a - b + 1 /\ 2*b - a - 1 >= 0 ]
		(1, 5)     evalgcdstart(a, b) -> evalgcdbb7in(b - a, a) [ a >= 1 /\ b >= 1 /\ b >= a + 1 /\ b - a - 1 >= 0 ]
		(?, 3)     evalgcdbb7in(a, b) -> evalgcdbb7in(a, b - a) [ b >= a + 1 /\ b >= a /\ -a + b >= 0 ]
		(?, 3)     evalgcdbb7in(a, b) -> evalgcdbb7in(a - b, b) [ a >= b + 1 /\ a - b - 1 >= 0 ]
	start location:	evalgcdstart
	leaf cost:	4

By chaining the transition evalgcdstart(a, b) -> evalgcdbb7in(b, a - 5*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 ] with all transitions in problem 19, the following new transitions are obtained:
	evalgcdstart(a, b) -> evalgcdbb7in(b, a - 6*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 ]
	evalgcdstart(a, b) -> evalgcdbb7in(6*b - a, a - 5*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ b >= a - 5*b + 1 /\ 6*b - a - 1 >= 0 ]
We thus obtain the following problem:
20:	T:
		(1, 20)    evalgcdstart(a, b) -> evalgcdbb7in(b, a - 6*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 ]
		(1, 20)    evalgcdstart(a, b) -> evalgcdbb7in(6*b - a, a - 5*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ b >= a - 5*b + 1 /\ 6*b - a - 1 >= 0 ]
		(1, 17)    evalgcdstart(a, b) -> evalgcdbb7in(5*b - a, a - 4*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ b >= a - 4*b + 1 /\ 5*b - a - 1 >= 0 ]
		(1, 14)    evalgcdstart(a, b) -> evalgcdbb7in(4*b - a, a - 3*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ b >= a - 3*b + 1 /\ 4*b - a - 1 >= 0 ]
		(1, 11)    evalgcdstart(a, b) -> evalgcdbb7in(3*b - a, a - 2*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ b >= a - 2*b + 1 /\ 3*b - a - 1 >= 0 ]
		(1, 8)     evalgcdstart(a, b) -> evalgcdbb7in(2*b - a, a - b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ b >= a - b + 1 /\ 2*b - a - 1 >= 0 ]
		(1, 5)     evalgcdstart(a, b) -> evalgcdbb7in(b - a, a) [ a >= 1 /\ b >= 1 /\ b >= a + 1 /\ b - a - 1 >= 0 ]
		(?, 3)     evalgcdbb7in(a, b) -> evalgcdbb7in(a, b - a) [ b >= a + 1 /\ b >= a /\ -a + b >= 0 ]
		(?, 3)     evalgcdbb7in(a, b) -> evalgcdbb7in(a - b, b) [ a >= b + 1 /\ a - b - 1 >= 0 ]
	start location:	evalgcdstart
	leaf cost:	4

By chaining the transition evalgcdstart(a, b) -> evalgcdbb7in(b, a - 6*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 ] with all transitions in problem 20, the following new transitions are obtained:
	evalgcdstart(a, b) -> evalgcdbb7in(b, a - 7*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ a - 6*b >= b + 1 /\ a - 6*b >= b /\ -7*b + a >= 0 ]
	evalgcdstart(a, b) -> evalgcdbb7in(7*b - a, a - 6*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ b >= a - 6*b + 1 /\ 7*b - a - 1 >= 0 ]
We thus obtain the following problem:
21:	T:
		(1, 23)    evalgcdstart(a, b) -> evalgcdbb7in(b, a - 7*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ a - 6*b >= b + 1 /\ a - 6*b >= b /\ -7*b + a >= 0 ]
		(1, 23)    evalgcdstart(a, b) -> evalgcdbb7in(7*b - a, a - 6*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ b >= a - 6*b + 1 /\ 7*b - a - 1 >= 0 ]
		(1, 20)    evalgcdstart(a, b) -> evalgcdbb7in(6*b - a, a - 5*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ b >= a - 5*b + 1 /\ 6*b - a - 1 >= 0 ]
		(1, 17)    evalgcdstart(a, b) -> evalgcdbb7in(5*b - a, a - 4*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ b >= a - 4*b + 1 /\ 5*b - a - 1 >= 0 ]
		(1, 14)    evalgcdstart(a, b) -> evalgcdbb7in(4*b - a, a - 3*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ b >= a - 3*b + 1 /\ 4*b - a - 1 >= 0 ]
		(1, 11)    evalgcdstart(a, b) -> evalgcdbb7in(3*b - a, a - 2*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ b >= a - 2*b + 1 /\ 3*b - a - 1 >= 0 ]
		(1, 8)     evalgcdstart(a, b) -> evalgcdbb7in(2*b - a, a - b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ b >= a - b + 1 /\ 2*b - a - 1 >= 0 ]
		(1, 5)     evalgcdstart(a, b) -> evalgcdbb7in(b - a, a) [ a >= 1 /\ b >= 1 /\ b >= a + 1 /\ b - a - 1 >= 0 ]
		(?, 3)     evalgcdbb7in(a, b) -> evalgcdbb7in(a, b - a) [ b >= a + 1 /\ b >= a /\ -a + b >= 0 ]
		(?, 3)     evalgcdbb7in(a, b) -> evalgcdbb7in(a - b, b) [ a >= b + 1 /\ a - b - 1 >= 0 ]
	start location:	evalgcdstart
	leaf cost:	4

By chaining the transition evalgcdstart(a, b) -> evalgcdbb7in(b, a - 7*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ a - 6*b >= b + 1 /\ a - 6*b >= b /\ -7*b + a >= 0 ] with all transitions in problem 21, the following new transitions are obtained:
	evalgcdstart(a, b) -> evalgcdbb7in(b, a - 8*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ a - 6*b >= b + 1 /\ a - 6*b >= b /\ -7*b + a >= 0 /\ a - 7*b >= b + 1 /\ a - 7*b >= b /\ -8*b + a >= 0 ]
	evalgcdstart(a, b) -> evalgcdbb7in(8*b - a, a - 7*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ a - 6*b >= b + 1 /\ a - 6*b >= b /\ -7*b + a >= 0 /\ b >= a - 7*b + 1 /\ 8*b - a - 1 >= 0 ]
We thus obtain the following problem:
22:	T:
		(1, 26)    evalgcdstart(a, b) -> evalgcdbb7in(b, a - 8*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ a - 6*b >= b + 1 /\ a - 6*b >= b /\ -7*b + a >= 0 /\ a - 7*b >= b + 1 /\ a - 7*b >= b /\ -8*b + a >= 0 ]
		(1, 26)    evalgcdstart(a, b) -> evalgcdbb7in(8*b - a, a - 7*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ a - 6*b >= b + 1 /\ a - 6*b >= b /\ -7*b + a >= 0 /\ b >= a - 7*b + 1 /\ 8*b - a - 1 >= 0 ]
		(1, 23)    evalgcdstart(a, b) -> evalgcdbb7in(7*b - a, a - 6*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ b >= a - 6*b + 1 /\ 7*b - a - 1 >= 0 ]
		(1, 20)    evalgcdstart(a, b) -> evalgcdbb7in(6*b - a, a - 5*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ b >= a - 5*b + 1 /\ 6*b - a - 1 >= 0 ]
		(1, 17)    evalgcdstart(a, b) -> evalgcdbb7in(5*b - a, a - 4*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ b >= a - 4*b + 1 /\ 5*b - a - 1 >= 0 ]
		(1, 14)    evalgcdstart(a, b) -> evalgcdbb7in(4*b - a, a - 3*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ b >= a - 3*b + 1 /\ 4*b - a - 1 >= 0 ]
		(1, 11)    evalgcdstart(a, b) -> evalgcdbb7in(3*b - a, a - 2*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ b >= a - 2*b + 1 /\ 3*b - a - 1 >= 0 ]
		(1, 8)     evalgcdstart(a, b) -> evalgcdbb7in(2*b - a, a - b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ b >= a - b + 1 /\ 2*b - a - 1 >= 0 ]
		(1, 5)     evalgcdstart(a, b) -> evalgcdbb7in(b - a, a) [ a >= 1 /\ b >= 1 /\ b >= a + 1 /\ b - a - 1 >= 0 ]
		(?, 3)     evalgcdbb7in(a, b) -> evalgcdbb7in(a, b - a) [ b >= a + 1 /\ b >= a /\ -a + b >= 0 ]
		(?, 3)     evalgcdbb7in(a, b) -> evalgcdbb7in(a - b, b) [ a >= b + 1 /\ a - b - 1 >= 0 ]
	start location:	evalgcdstart
	leaf cost:	4

By chaining the transition evalgcdstart(a, b) -> evalgcdbb7in(b, a - 8*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ a - 6*b >= b + 1 /\ a - 6*b >= b /\ -7*b + a >= 0 /\ a - 7*b >= b + 1 /\ a - 7*b >= b /\ -8*b + a >= 0 ] with all transitions in problem 22, the following new transitions are obtained:
	evalgcdstart(a, b) -> evalgcdbb7in(b, a - 9*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ a - 6*b >= b + 1 /\ a - 6*b >= b /\ -7*b + a >= 0 /\ a - 7*b >= b + 1 /\ a - 7*b >= b /\ -8*b + a >= 0 /\ a - 8*b >= b + 1 /\ a - 8*b >= b /\ -9*b + a >= 0 ]
	evalgcdstart(a, b) -> evalgcdbb7in(9*b - a, a - 8*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ a - 6*b >= b + 1 /\ a - 6*b >= b /\ -7*b + a >= 0 /\ a - 7*b >= b + 1 /\ a - 7*b >= b /\ -8*b + a >= 0 /\ b >= a - 8*b + 1 /\ 9*b - a - 1 >= 0 ]
We thus obtain the following problem:
23:	T:
		(1, 29)    evalgcdstart(a, b) -> evalgcdbb7in(b, a - 9*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ a - 6*b >= b + 1 /\ a - 6*b >= b /\ -7*b + a >= 0 /\ a - 7*b >= b + 1 /\ a - 7*b >= b /\ -8*b + a >= 0 /\ a - 8*b >= b + 1 /\ a - 8*b >= b /\ -9*b + a >= 0 ]
		(1, 29)    evalgcdstart(a, b) -> evalgcdbb7in(9*b - a, a - 8*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ a - 6*b >= b + 1 /\ a - 6*b >= b /\ -7*b + a >= 0 /\ a - 7*b >= b + 1 /\ a - 7*b >= b /\ -8*b + a >= 0 /\ b >= a - 8*b + 1 /\ 9*b - a - 1 >= 0 ]
		(1, 26)    evalgcdstart(a, b) -> evalgcdbb7in(8*b - a, a - 7*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ a - 6*b >= b + 1 /\ a - 6*b >= b /\ -7*b + a >= 0 /\ b >= a - 7*b + 1 /\ 8*b - a - 1 >= 0 ]
		(1, 23)    evalgcdstart(a, b) -> evalgcdbb7in(7*b - a, a - 6*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ b >= a - 6*b + 1 /\ 7*b - a - 1 >= 0 ]
		(1, 20)    evalgcdstart(a, b) -> evalgcdbb7in(6*b - a, a - 5*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ b >= a - 5*b + 1 /\ 6*b - a - 1 >= 0 ]
		(1, 17)    evalgcdstart(a, b) -> evalgcdbb7in(5*b - a, a - 4*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ b >= a - 4*b + 1 /\ 5*b - a - 1 >= 0 ]
		(1, 14)    evalgcdstart(a, b) -> evalgcdbb7in(4*b - a, a - 3*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ b >= a - 3*b + 1 /\ 4*b - a - 1 >= 0 ]
		(1, 11)    evalgcdstart(a, b) -> evalgcdbb7in(3*b - a, a - 2*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ b >= a - 2*b + 1 /\ 3*b - a - 1 >= 0 ]
		(1, 8)     evalgcdstart(a, b) -> evalgcdbb7in(2*b - a, a - b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ b >= a - b + 1 /\ 2*b - a - 1 >= 0 ]
		(1, 5)     evalgcdstart(a, b) -> evalgcdbb7in(b - a, a) [ a >= 1 /\ b >= 1 /\ b >= a + 1 /\ b - a - 1 >= 0 ]
		(?, 3)     evalgcdbb7in(a, b) -> evalgcdbb7in(a, b - a) [ b >= a + 1 /\ b >= a /\ -a + b >= 0 ]
		(?, 3)     evalgcdbb7in(a, b) -> evalgcdbb7in(a - b, b) [ a >= b + 1 /\ a - b - 1 >= 0 ]
	start location:	evalgcdstart
	leaf cost:	4

By chaining the transition evalgcdstart(a, b) -> evalgcdbb7in(b, a - 9*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ a - 6*b >= b + 1 /\ a - 6*b >= b /\ -7*b + a >= 0 /\ a - 7*b >= b + 1 /\ a - 7*b >= b /\ -8*b + a >= 0 /\ a - 8*b >= b + 1 /\ a - 8*b >= b /\ -9*b + a >= 0 ] with all transitions in problem 23, the following new transitions are obtained:
	evalgcdstart(a, b) -> evalgcdbb7in(b, a - 10*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ a - 6*b >= b + 1 /\ a - 6*b >= b /\ -7*b + a >= 0 /\ a - 7*b >= b + 1 /\ a - 7*b >= b /\ -8*b + a >= 0 /\ a - 8*b >= b + 1 /\ a - 8*b >= b /\ -9*b + a >= 0 /\ a - 9*b >= b + 1 /\ a - 9*b >= b /\ -10*b + a >= 0 ]
	evalgcdstart(a, b) -> evalgcdbb7in(10*b - a, a - 9*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ a - 6*b >= b + 1 /\ a - 6*b >= b /\ -7*b + a >= 0 /\ a - 7*b >= b + 1 /\ a - 7*b >= b /\ -8*b + a >= 0 /\ a - 8*b >= b + 1 /\ a - 8*b >= b /\ -9*b + a >= 0 /\ b >= a - 9*b + 1 /\ 10*b - a - 1 >= 0 ]
We thus obtain the following problem:
24:	T:
		(1, 32)    evalgcdstart(a, b) -> evalgcdbb7in(b, a - 10*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ a - 6*b >= b + 1 /\ a - 6*b >= b /\ -7*b + a >= 0 /\ a - 7*b >= b + 1 /\ a - 7*b >= b /\ -8*b + a >= 0 /\ a - 8*b >= b + 1 /\ a - 8*b >= b /\ -9*b + a >= 0 /\ a - 9*b >= b + 1 /\ a - 9*b >= b /\ -10*b + a >= 0 ]
		(1, 32)    evalgcdstart(a, b) -> evalgcdbb7in(10*b - a, a - 9*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ a - 6*b >= b + 1 /\ a - 6*b >= b /\ -7*b + a >= 0 /\ a - 7*b >= b + 1 /\ a - 7*b >= b /\ -8*b + a >= 0 /\ a - 8*b >= b + 1 /\ a - 8*b >= b /\ -9*b + a >= 0 /\ b >= a - 9*b + 1 /\ 10*b - a - 1 >= 0 ]
		(1, 29)    evalgcdstart(a, b) -> evalgcdbb7in(9*b - a, a - 8*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ a - 6*b >= b + 1 /\ a - 6*b >= b /\ -7*b + a >= 0 /\ a - 7*b >= b + 1 /\ a - 7*b >= b /\ -8*b + a >= 0 /\ b >= a - 8*b + 1 /\ 9*b - a - 1 >= 0 ]
		(1, 26)    evalgcdstart(a, b) -> evalgcdbb7in(8*b - a, a - 7*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ a - 6*b >= b + 1 /\ a - 6*b >= b /\ -7*b + a >= 0 /\ b >= a - 7*b + 1 /\ 8*b - a - 1 >= 0 ]
		(1, 23)    evalgcdstart(a, b) -> evalgcdbb7in(7*b - a, a - 6*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ a - 5*b >= b + 1 /\ a - 5*b >= b /\ -6*b + a >= 0 /\ b >= a - 6*b + 1 /\ 7*b - a - 1 >= 0 ]
		(1, 20)    evalgcdstart(a, b) -> evalgcdbb7in(6*b - a, a - 5*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ a - 4*b >= b + 1 /\ a - 4*b >= b /\ -5*b + a >= 0 /\ b >= a - 5*b + 1 /\ 6*b - a - 1 >= 0 ]
		(1, 17)    evalgcdstart(a, b) -> evalgcdbb7in(5*b - a, a - 4*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ a - 3*b >= b + 1 /\ a - 3*b >= b /\ -4*b + a >= 0 /\ b >= a - 4*b + 1 /\ 5*b - a - 1 >= 0 ]
		(1, 14)    evalgcdstart(a, b) -> evalgcdbb7in(4*b - a, a - 3*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ a - 2*b >= b + 1 /\ a - 2*b >= b /\ -3*b + a >= 0 /\ b >= a - 3*b + 1 /\ 4*b - a - 1 >= 0 ]
		(1, 11)    evalgcdstart(a, b) -> evalgcdbb7in(3*b - a, a - 2*b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ a - b >= b + 1 /\ a - b >= b /\ -2*b + a >= 0 /\ b >= a - 2*b + 1 /\ 3*b - a - 1 >= 0 ]
		(1, 8)     evalgcdstart(a, b) -> evalgcdbb7in(2*b - a, a - b) [ a >= 1 /\ b >= 1 /\ a >= b + 1 /\ a >= b /\ -b + a >= 0 /\ b >= a - b + 1 /\ 2*b - a - 1 >= 0 ]
		(1, 5)     evalgcdstart(a, b) -> evalgcdbb7in(b - a, a) [ a >= 1 /\ b >= 1 /\ b >= a + 1 /\ b - a - 1 >= 0 ]
		(?, 3)     evalgcdbb7in(a, b) -> evalgcdbb7in(a, b - a) [ b >= a + 1 /\ b >= a /\ -a + b >= 0 ]
		(?, 3)     evalgcdbb7in(a, b) -> evalgcdbb7in(a - b, b) [ a >= b + 1 /\ a - b - 1 >= 0 ]
	start location:	evalgcdstart
	leaf cost:	4

Complexity upper bound ?

Time: 3.370 sec (SMT: 3.151 sec)