MAYBE

Initial complexity problem:
1:	T:
		(1, 1)    evalcousot9start(a, b, c) -> evalcousot9entryin(a, b, c)
		(?, 1)    evalcousot9entryin(a, b, c) -> evalcousot9bb3in(d, c, c)
		(?, 1)    evalcousot9bb3in(a, b, c) -> evalcousot9bbin(a, b, c) [ b >= 1 ]
		(?, 1)    evalcousot9bb3in(a, b, c) -> evalcousot9returnin(a, b, c) [ 0 >= b ]
		(?, 1)    evalcousot9bbin(a, b, c) -> evalcousot9bb1in(a, b, c) [ a >= 1 ]
		(?, 1)    evalcousot9bbin(a, b, c) -> evalcousot9bb2in(a, b, c) [ 0 >= a ]
		(?, 1)    evalcousot9bb1in(a, b, c) -> evalcousot9bb3in(a - 1, b, c)
		(?, 1)    evalcousot9bb2in(a, b, c) -> evalcousot9bb3in(c, b - 1, c)
		(?, 1)    evalcousot9returnin(a, b, c) -> evalcousot9stop(a, b, c)
	start location:	evalcousot9start
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalcousot9start(a, b, c) -> evalcousot9entryin(a, b, c)
		(?, 1)    evalcousot9entryin(a, b, c) -> evalcousot9bb3in(d, c, c)
		(?, 1)    evalcousot9bb3in(a, b, c) -> evalcousot9bbin(a, b, c) [ b >= 1 ]
		(?, 1)    evalcousot9bbin(a, b, c) -> evalcousot9bb1in(a, b, c) [ a >= 1 ]
		(?, 1)    evalcousot9bbin(a, b, c) -> evalcousot9bb2in(a, b, c) [ 0 >= a ]
		(?, 1)    evalcousot9bb1in(a, b, c) -> evalcousot9bb3in(a - 1, b, c)
		(?, 1)    evalcousot9bb2in(a, b, c) -> evalcousot9bb3in(c, b - 1, c)
	start location:	evalcousot9start
	leaf cost:	2

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalcousot9start(a, b, c) -> evalcousot9entryin(a, b, c)
		(1, 1)    evalcousot9entryin(a, b, c) -> evalcousot9bb3in(d, c, c)
		(?, 1)    evalcousot9bb3in(a, b, c) -> evalcousot9bbin(a, b, c) [ b >= 1 ]
		(?, 1)    evalcousot9bbin(a, b, c) -> evalcousot9bb1in(a, b, c) [ a >= 1 ]
		(?, 1)    evalcousot9bbin(a, b, c) -> evalcousot9bb2in(a, b, c) [ 0 >= a ]
		(?, 1)    evalcousot9bb1in(a, b, c) -> evalcousot9bb3in(a - 1, b, c)
		(?, 1)    evalcousot9bb2in(a, b, c) -> evalcousot9bb3in(c, b - 1, c)
	start location:	evalcousot9start
	leaf cost:	2

Applied AI with 'oct' on problem 3 to obtain the following invariants:
  For symbol evalcousot9bb1in: X_3 - 1 >= 0 /\ X_2 + X_3 - 2 >= 0 /\ -X_2 + X_3 >= 0 /\ X_1 + X_3 - 2 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ X_1 - 1 >= 0
  For symbol evalcousot9bb2in: X_3 - 1 >= 0 /\ X_2 + X_3 - 2 >= 0 /\ -X_2 + X_3 >= 0 /\ -X_1 + X_3 - 1 >= 0 /\ X_2 - 1 >= 0 /\ -X_1 + X_2 - 1 >= 0 /\ -X_1 >= 0
  For symbol evalcousot9bb3in: -X_2 + X_3 >= 0
  For symbol evalcousot9bbin: X_3 - 1 >= 0 /\ X_2 + X_3 - 2 >= 0 /\ -X_2 + X_3 >= 0 /\ X_2 - 1 >= 0


This yielded the following problem:
4:	T:
		(?, 1)    evalcousot9bb2in(a, b, c) -> evalcousot9bb3in(c, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 ]
		(?, 1)    evalcousot9bb1in(a, b, c) -> evalcousot9bb3in(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(?, 1)    evalcousot9bbin(a, b, c) -> evalcousot9bb2in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a ]
		(?, 1)    evalcousot9bbin(a, b, c) -> evalcousot9bb1in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 ]
		(?, 1)    evalcousot9bb3in(a, b, c) -> evalcousot9bbin(a, b, c) [ -b + c >= 0 /\ b >= 1 ]
		(1, 1)    evalcousot9entryin(a, b, c) -> evalcousot9bb3in(d, c, c)
		(1, 1)    evalcousot9start(a, b, c) -> evalcousot9entryin(a, b, c)
	start location:	evalcousot9start
	leaf cost:	2

A polynomial rank function with
	Pol(evalcousot9bb2in) = 2*V_2 + 2*V_3 - 3
	Pol(evalcousot9bb3in) = 2*V_2 + 2*V_3 - 2
	Pol(evalcousot9bb1in) = 2*V_2 + 2*V_3 - 2
	Pol(evalcousot9bbin) = 2*V_2 + 2*V_3 - 2
	Pol(evalcousot9entryin) = 4*V_3 - 2
	Pol(evalcousot9start) = 4*V_3 - 2
orients all transitions weakly and the transitions
	evalcousot9bbin(a, b, c) -> evalcousot9bb2in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a ]
	evalcousot9bb2in(a, b, c) -> evalcousot9bb3in(c, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 ]
strictly and produces the following problem:
5:	T:
		(4*c + 2, 1)    evalcousot9bb2in(a, b, c) -> evalcousot9bb3in(c, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 ]
		(?, 1)          evalcousot9bb1in(a, b, c) -> evalcousot9bb3in(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(4*c + 2, 1)    evalcousot9bbin(a, b, c) -> evalcousot9bb2in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a ]
		(?, 1)          evalcousot9bbin(a, b, c) -> evalcousot9bb1in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 ]
		(?, 1)          evalcousot9bb3in(a, b, c) -> evalcousot9bbin(a, b, c) [ -b + c >= 0 /\ b >= 1 ]
		(1, 1)          evalcousot9entryin(a, b, c) -> evalcousot9bb3in(d, c, c)
		(1, 1)          evalcousot9start(a, b, c) -> evalcousot9entryin(a, b, c)
	start location:	evalcousot9start
	leaf cost:	2

By chaining the transition evalcousot9bb2in(a, b, c) -> evalcousot9bb3in(c, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 ] with all transitions in problem 5, the following new transition is obtained:
	evalcousot9bb2in(a, b, c) -> evalcousot9bbin(c, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 ]
We thus obtain the following problem:
6:	T:
		(4*c + 2, 2)    evalcousot9bb2in(a, b, c) -> evalcousot9bbin(c, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 ]
		(?, 1)          evalcousot9bb1in(a, b, c) -> evalcousot9bb3in(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(4*c + 2, 1)    evalcousot9bbin(a, b, c) -> evalcousot9bb2in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a ]
		(?, 1)          evalcousot9bbin(a, b, c) -> evalcousot9bb1in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 ]
		(?, 1)          evalcousot9bb3in(a, b, c) -> evalcousot9bbin(a, b, c) [ -b + c >= 0 /\ b >= 1 ]
		(1, 1)          evalcousot9entryin(a, b, c) -> evalcousot9bb3in(d, c, c)
		(1, 1)          evalcousot9start(a, b, c) -> evalcousot9entryin(a, b, c)
	start location:	evalcousot9start
	leaf cost:	2

By chaining the transition evalcousot9bb2in(a, b, c) -> evalcousot9bbin(c, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 ] with all transitions in problem 6, the following new transition is obtained:
	evalcousot9bb2in(a, b, c) -> evalcousot9bb1in(c, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 ]
We thus obtain the following problem:
7:	T:
		(4*c + 2, 3)    evalcousot9bb2in(a, b, c) -> evalcousot9bb1in(c, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 ]
		(?, 1)          evalcousot9bb1in(a, b, c) -> evalcousot9bb3in(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(4*c + 2, 1)    evalcousot9bbin(a, b, c) -> evalcousot9bb2in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a ]
		(?, 1)          evalcousot9bbin(a, b, c) -> evalcousot9bb1in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 ]
		(?, 1)          evalcousot9bb3in(a, b, c) -> evalcousot9bbin(a, b, c) [ -b + c >= 0 /\ b >= 1 ]
		(1, 1)          evalcousot9entryin(a, b, c) -> evalcousot9bb3in(d, c, c)
		(1, 1)          evalcousot9start(a, b, c) -> evalcousot9entryin(a, b, c)
	start location:	evalcousot9start
	leaf cost:	2

By chaining the transition evalcousot9bb2in(a, b, c) -> evalcousot9bb1in(c, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 ] with all transitions in problem 7, the following new transition is obtained:
	evalcousot9bb2in(a, b, c) -> evalcousot9bb3in(c - 1, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 ]
We thus obtain the following problem:
8:	T:
		(4*c + 2, 4)    evalcousot9bb2in(a, b, c) -> evalcousot9bb3in(c - 1, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 ]
		(?, 1)          evalcousot9bb1in(a, b, c) -> evalcousot9bb3in(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(4*c + 2, 1)    evalcousot9bbin(a, b, c) -> evalcousot9bb2in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a ]
		(?, 1)          evalcousot9bbin(a, b, c) -> evalcousot9bb1in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 ]
		(?, 1)          evalcousot9bb3in(a, b, c) -> evalcousot9bbin(a, b, c) [ -b + c >= 0 /\ b >= 1 ]
		(1, 1)          evalcousot9entryin(a, b, c) -> evalcousot9bb3in(d, c, c)
		(1, 1)          evalcousot9start(a, b, c) -> evalcousot9entryin(a, b, c)
	start location:	evalcousot9start
	leaf cost:	2

By chaining the transition evalcousot9bb2in(a, b, c) -> evalcousot9bb3in(c - 1, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 ] with all transitions in problem 8, the following new transition is obtained:
	evalcousot9bb2in(a, b, c) -> evalcousot9bbin(c - 1, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 ]
We thus obtain the following problem:
9:	T:
		(4*c + 2, 5)    evalcousot9bb2in(a, b, c) -> evalcousot9bbin(c - 1, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 ]
		(?, 1)          evalcousot9bb1in(a, b, c) -> evalcousot9bb3in(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(4*c + 2, 1)    evalcousot9bbin(a, b, c) -> evalcousot9bb2in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a ]
		(?, 1)          evalcousot9bbin(a, b, c) -> evalcousot9bb1in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 ]
		(?, 1)          evalcousot9bb3in(a, b, c) -> evalcousot9bbin(a, b, c) [ -b + c >= 0 /\ b >= 1 ]
		(1, 1)          evalcousot9entryin(a, b, c) -> evalcousot9bb3in(d, c, c)
		(1, 1)          evalcousot9start(a, b, c) -> evalcousot9entryin(a, b, c)
	start location:	evalcousot9start
	leaf cost:	2

By chaining the transition evalcousot9bb2in(a, b, c) -> evalcousot9bbin(c - 1, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 ] with all transitions in problem 9, the following new transition is obtained:
	evalcousot9bb2in(a, b, c) -> evalcousot9bb1in(c - 1, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 ]
We thus obtain the following problem:
10:	T:
		(4*c + 2, 6)    evalcousot9bb2in(a, b, c) -> evalcousot9bb1in(c - 1, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 ]
		(?, 1)          evalcousot9bb1in(a, b, c) -> evalcousot9bb3in(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(4*c + 2, 1)    evalcousot9bbin(a, b, c) -> evalcousot9bb2in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a ]
		(?, 1)          evalcousot9bbin(a, b, c) -> evalcousot9bb1in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 ]
		(?, 1)          evalcousot9bb3in(a, b, c) -> evalcousot9bbin(a, b, c) [ -b + c >= 0 /\ b >= 1 ]
		(1, 1)          evalcousot9entryin(a, b, c) -> evalcousot9bb3in(d, c, c)
		(1, 1)          evalcousot9start(a, b, c) -> evalcousot9entryin(a, b, c)
	start location:	evalcousot9start
	leaf cost:	2

By chaining the transition evalcousot9bb2in(a, b, c) -> evalcousot9bb1in(c - 1, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 ] with all transitions in problem 10, the following new transition is obtained:
	evalcousot9bb2in(a, b, c) -> evalcousot9bb3in(c - 2, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 ]
We thus obtain the following problem:
11:	T:
		(4*c + 2, 7)    evalcousot9bb2in(a, b, c) -> evalcousot9bb3in(c - 2, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 ]
		(?, 1)          evalcousot9bb1in(a, b, c) -> evalcousot9bb3in(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(4*c + 2, 1)    evalcousot9bbin(a, b, c) -> evalcousot9bb2in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a ]
		(?, 1)          evalcousot9bbin(a, b, c) -> evalcousot9bb1in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 ]
		(?, 1)          evalcousot9bb3in(a, b, c) -> evalcousot9bbin(a, b, c) [ -b + c >= 0 /\ b >= 1 ]
		(1, 1)          evalcousot9entryin(a, b, c) -> evalcousot9bb3in(d, c, c)
		(1, 1)          evalcousot9start(a, b, c) -> evalcousot9entryin(a, b, c)
	start location:	evalcousot9start
	leaf cost:	2

By chaining the transition evalcousot9bb2in(a, b, c) -> evalcousot9bb3in(c - 2, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 ] with all transitions in problem 11, the following new transition is obtained:
	evalcousot9bb2in(a, b, c) -> evalcousot9bbin(c - 2, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 ]
We thus obtain the following problem:
12:	T:
		(4*c + 2, 8)    evalcousot9bb2in(a, b, c) -> evalcousot9bbin(c - 2, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 ]
		(?, 1)          evalcousot9bb1in(a, b, c) -> evalcousot9bb3in(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(4*c + 2, 1)    evalcousot9bbin(a, b, c) -> evalcousot9bb2in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a ]
		(?, 1)          evalcousot9bbin(a, b, c) -> evalcousot9bb1in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 ]
		(?, 1)          evalcousot9bb3in(a, b, c) -> evalcousot9bbin(a, b, c) [ -b + c >= 0 /\ b >= 1 ]
		(1, 1)          evalcousot9entryin(a, b, c) -> evalcousot9bb3in(d, c, c)
		(1, 1)          evalcousot9start(a, b, c) -> evalcousot9entryin(a, b, c)
	start location:	evalcousot9start
	leaf cost:	2

By chaining the transition evalcousot9bb1in(a, b, c) -> evalcousot9bb3in(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ] with all transitions in problem 12, the following new transition is obtained:
	evalcousot9bb1in(a, b, c) -> evalcousot9bbin(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= 1 ]
We thus obtain the following problem:
13:	T:
		(?, 2)          evalcousot9bb1in(a, b, c) -> evalcousot9bbin(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= 1 ]
		(4*c + 2, 8)    evalcousot9bb2in(a, b, c) -> evalcousot9bbin(c - 2, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 ]
		(4*c + 2, 1)    evalcousot9bbin(a, b, c) -> evalcousot9bb2in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a ]
		(?, 1)          evalcousot9bbin(a, b, c) -> evalcousot9bb1in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 ]
		(?, 1)          evalcousot9bb3in(a, b, c) -> evalcousot9bbin(a, b, c) [ -b + c >= 0 /\ b >= 1 ]
		(1, 1)          evalcousot9entryin(a, b, c) -> evalcousot9bb3in(d, c, c)
		(1, 1)          evalcousot9start(a, b, c) -> evalcousot9entryin(a, b, c)
	start location:	evalcousot9start
	leaf cost:	2

Repeatedly propagating knowledge in problem 13 produces the following problem:
14:	T:
		(?, 2)          evalcousot9bb1in(a, b, c) -> evalcousot9bbin(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= 1 ]
		(4*c + 2, 8)    evalcousot9bb2in(a, b, c) -> evalcousot9bbin(c - 2, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 ]
		(4*c + 2, 1)    evalcousot9bbin(a, b, c) -> evalcousot9bb2in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a ]
		(?, 1)          evalcousot9bbin(a, b, c) -> evalcousot9bb1in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 ]
		(1, 1)          evalcousot9bb3in(a, b, c) -> evalcousot9bbin(a, b, c) [ -b + c >= 0 /\ b >= 1 ]
		(1, 1)          evalcousot9entryin(a, b, c) -> evalcousot9bb3in(d, c, c)
		(1, 1)          evalcousot9start(a, b, c) -> evalcousot9entryin(a, b, c)
	start location:	evalcousot9start
	leaf cost:	2

By chaining the transition evalcousot9bbin(a, b, c) -> evalcousot9bb2in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a ] with all transitions in problem 14, the following new transition is obtained:
	evalcousot9bbin(a, b, c) -> evalcousot9bbin(c - 2, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a /\ -a + c - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 ]
We thus obtain the following problem:
15:	T:
		(4*c + 2, 9)    evalcousot9bbin(a, b, c) -> evalcousot9bbin(c - 2, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a /\ -a + c - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 ]
		(?, 2)          evalcousot9bb1in(a, b, c) -> evalcousot9bbin(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= 1 ]
		(4*c + 2, 8)    evalcousot9bb2in(a, b, c) -> evalcousot9bbin(c - 2, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 ]
		(?, 1)          evalcousot9bbin(a, b, c) -> evalcousot9bb1in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 ]
		(1, 1)          evalcousot9bb3in(a, b, c) -> evalcousot9bbin(a, b, c) [ -b + c >= 0 /\ b >= 1 ]
		(1, 1)          evalcousot9entryin(a, b, c) -> evalcousot9bb3in(d, c, c)
		(1, 1)          evalcousot9start(a, b, c) -> evalcousot9entryin(a, b, c)
	start location:	evalcousot9start
	leaf cost:	2

Testing for reachability in the complexity graph removes the following transition from problem 15:
	evalcousot9bb2in(a, b, c) -> evalcousot9bbin(c - 2, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 ]
We thus obtain the following problem:
16:	T:
		(?, 2)          evalcousot9bb1in(a, b, c) -> evalcousot9bbin(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= 1 ]
		(4*c + 2, 9)    evalcousot9bbin(a, b, c) -> evalcousot9bbin(c - 2, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a /\ -a + c - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 ]
		(?, 1)          evalcousot9bbin(a, b, c) -> evalcousot9bb1in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 ]
		(1, 1)          evalcousot9bb3in(a, b, c) -> evalcousot9bbin(a, b, c) [ -b + c >= 0 /\ b >= 1 ]
		(1, 1)          evalcousot9entryin(a, b, c) -> evalcousot9bb3in(d, c, c)
		(1, 1)          evalcousot9start(a, b, c) -> evalcousot9entryin(a, b, c)
	start location:	evalcousot9start
	leaf cost:	2

By chaining the transition evalcousot9bbin(a, b, c) -> evalcousot9bbin(c - 2, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a /\ -a + c - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 ] with all transitions in problem 16, the following new transition is obtained:
	evalcousot9bbin(a, b, c) -> evalcousot9bb1in(c - 2, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a /\ -a + c - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 /\ c - 2 >= 1 ]
We thus obtain the following problem:
17:	T:
		(4*c + 2, 10)    evalcousot9bbin(a, b, c) -> evalcousot9bb1in(c - 2, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a /\ -a + c - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 /\ c - 2 >= 1 ]
		(?, 2)           evalcousot9bb1in(a, b, c) -> evalcousot9bbin(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= 1 ]
		(?, 1)           evalcousot9bbin(a, b, c) -> evalcousot9bb1in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 ]
		(1, 1)           evalcousot9bb3in(a, b, c) -> evalcousot9bbin(a, b, c) [ -b + c >= 0 /\ b >= 1 ]
		(1, 1)           evalcousot9entryin(a, b, c) -> evalcousot9bb3in(d, c, c)
		(1, 1)           evalcousot9start(a, b, c) -> evalcousot9entryin(a, b, c)
	start location:	evalcousot9start
	leaf cost:	2

By chaining the transition evalcousot9bbin(a, b, c) -> evalcousot9bb1in(c - 2, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a /\ -a + c - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 /\ c - 2 >= 1 ] with all transitions in problem 17, the following new transition is obtained:
	evalcousot9bbin(a, b, c) -> evalcousot9bbin(c - 3, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a /\ -a + c - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 /\ c - 2 >= 1 /\ 2*c - 4 >= 0 /\ c + b - 5 >= 0 /\ c - 3 >= 0 ]
We thus obtain the following problem:
18:	T:
		(4*c + 2, 12)    evalcousot9bbin(a, b, c) -> evalcousot9bbin(c - 3, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a /\ -a + c - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 /\ c - 2 >= 1 /\ 2*c - 4 >= 0 /\ c + b - 5 >= 0 /\ c - 3 >= 0 ]
		(?, 2)           evalcousot9bb1in(a, b, c) -> evalcousot9bbin(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= 1 ]
		(?, 1)           evalcousot9bbin(a, b, c) -> evalcousot9bb1in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 ]
		(1, 1)           evalcousot9bb3in(a, b, c) -> evalcousot9bbin(a, b, c) [ -b + c >= 0 /\ b >= 1 ]
		(1, 1)           evalcousot9entryin(a, b, c) -> evalcousot9bb3in(d, c, c)
		(1, 1)           evalcousot9start(a, b, c) -> evalcousot9entryin(a, b, c)
	start location:	evalcousot9start
	leaf cost:	2

By chaining the transition evalcousot9bbin(a, b, c) -> evalcousot9bb1in(a, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 ] with all transitions in problem 18, the following new transition is obtained:
	evalcousot9bbin(a, b, c) -> evalcousot9bbin(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 /\ a + c - 2 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= 1 ]
We thus obtain the following problem:
19:	T:
		(?, 3)           evalcousot9bbin(a, b, c) -> evalcousot9bbin(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 /\ a + c - 2 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= 1 ]
		(4*c + 2, 12)    evalcousot9bbin(a, b, c) -> evalcousot9bbin(c - 3, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a /\ -a + c - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 /\ c - 2 >= 1 /\ 2*c - 4 >= 0 /\ c + b - 5 >= 0 /\ c - 3 >= 0 ]
		(?, 2)           evalcousot9bb1in(a, b, c) -> evalcousot9bbin(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= 1 ]
		(1, 1)           evalcousot9bb3in(a, b, c) -> evalcousot9bbin(a, b, c) [ -b + c >= 0 /\ b >= 1 ]
		(1, 1)           evalcousot9entryin(a, b, c) -> evalcousot9bb3in(d, c, c)
		(1, 1)           evalcousot9start(a, b, c) -> evalcousot9entryin(a, b, c)
	start location:	evalcousot9start
	leaf cost:	2

Testing for reachability in the complexity graph removes the following transition from problem 19:
	evalcousot9bb1in(a, b, c) -> evalcousot9bbin(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= 1 ]
We thus obtain the following problem:
20:	T:
		(?, 3)           evalcousot9bbin(a, b, c) -> evalcousot9bbin(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 /\ a + c - 2 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= 1 ]
		(4*c + 2, 12)    evalcousot9bbin(a, b, c) -> evalcousot9bbin(c - 3, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a /\ -a + c - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 /\ c - 2 >= 1 /\ 2*c - 4 >= 0 /\ c + b - 5 >= 0 /\ c - 3 >= 0 ]
		(1, 1)           evalcousot9bb3in(a, b, c) -> evalcousot9bbin(a, b, c) [ -b + c >= 0 /\ b >= 1 ]
		(1, 1)           evalcousot9entryin(a, b, c) -> evalcousot9bb3in(d, c, c)
		(1, 1)           evalcousot9start(a, b, c) -> evalcousot9entryin(a, b, c)
	start location:	evalcousot9start
	leaf cost:	2

By chaining the transition evalcousot9entryin(a, b, c) -> evalcousot9bb3in(d, c, c) with all transitions in problem 20, the following new transition is obtained:
	evalcousot9entryin(a, b, c) -> evalcousot9bbin(d, c, c) [ 0 >= 0 /\ c >= 1 ]
We thus obtain the following problem:
21:	T:
		(1, 2)           evalcousot9entryin(a, b, c) -> evalcousot9bbin(d, c, c) [ 0 >= 0 /\ c >= 1 ]
		(?, 3)           evalcousot9bbin(a, b, c) -> evalcousot9bbin(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 /\ a + c - 2 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= 1 ]
		(4*c + 2, 12)    evalcousot9bbin(a, b, c) -> evalcousot9bbin(c - 3, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a /\ -a + c - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 /\ c - 2 >= 1 /\ 2*c - 4 >= 0 /\ c + b - 5 >= 0 /\ c - 3 >= 0 ]
		(1, 1)           evalcousot9bb3in(a, b, c) -> evalcousot9bbin(a, b, c) [ -b + c >= 0 /\ b >= 1 ]
		(1, 1)           evalcousot9start(a, b, c) -> evalcousot9entryin(a, b, c)
	start location:	evalcousot9start
	leaf cost:	2

Testing for reachability in the complexity graph removes the following transition from problem 21:
	evalcousot9bb3in(a, b, c) -> evalcousot9bbin(a, b, c) [ -b + c >= 0 /\ b >= 1 ]
We thus obtain the following problem:
22:	T:
		(?, 3)           evalcousot9bbin(a, b, c) -> evalcousot9bbin(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 /\ a + c - 2 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= 1 ]
		(4*c + 2, 12)    evalcousot9bbin(a, b, c) -> evalcousot9bbin(c - 3, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a /\ -a + c - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 /\ c - 2 >= 1 /\ 2*c - 4 >= 0 /\ c + b - 5 >= 0 /\ c - 3 >= 0 ]
		(1, 2)           evalcousot9entryin(a, b, c) -> evalcousot9bbin(d, c, c) [ 0 >= 0 /\ c >= 1 ]
		(1, 1)           evalcousot9start(a, b, c) -> evalcousot9entryin(a, b, c)
	start location:	evalcousot9start
	leaf cost:	2

By chaining the transition evalcousot9start(a, b, c) -> evalcousot9entryin(a, b, c) with all transitions in problem 22, the following new transition is obtained:
	evalcousot9start(a, b, c) -> evalcousot9bbin(d, c, c) [ 0 >= 0 /\ c >= 1 ]
We thus obtain the following problem:
23:	T:
		(1, 3)           evalcousot9start(a, b, c) -> evalcousot9bbin(d, c, c) [ 0 >= 0 /\ c >= 1 ]
		(?, 3)           evalcousot9bbin(a, b, c) -> evalcousot9bbin(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 /\ a + c - 2 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= 1 ]
		(4*c + 2, 12)    evalcousot9bbin(a, b, c) -> evalcousot9bbin(c - 3, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a /\ -a + c - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 /\ c - 2 >= 1 /\ 2*c - 4 >= 0 /\ c + b - 5 >= 0 /\ c - 3 >= 0 ]
		(1, 2)           evalcousot9entryin(a, b, c) -> evalcousot9bbin(d, c, c) [ 0 >= 0 /\ c >= 1 ]
	start location:	evalcousot9start
	leaf cost:	2

Testing for reachability in the complexity graph removes the following transition from problem 23:
	evalcousot9entryin(a, b, c) -> evalcousot9bbin(d, c, c) [ 0 >= 0 /\ c >= 1 ]
We thus obtain the following problem:
24:	T:
		(?, 3)           evalcousot9bbin(a, b, c) -> evalcousot9bbin(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 /\ a + c - 2 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= 1 ]
		(4*c + 2, 12)    evalcousot9bbin(a, b, c) -> evalcousot9bbin(c - 3, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a /\ -a + c - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 /\ c - 2 >= 1 /\ 2*c - 4 >= 0 /\ c + b - 5 >= 0 /\ c - 3 >= 0 ]
		(1, 3)           evalcousot9start(a, b, c) -> evalcousot9bbin(d, c, c) [ 0 >= 0 /\ c >= 1 ]
	start location:	evalcousot9start
	leaf cost:	2

By chaining the transition evalcousot9start(a, b, c) -> evalcousot9bbin(d, c, c) [ 0 >= 0 /\ c >= 1 ] with all transitions in problem 24, the following new transitions are obtained:
	evalcousot9start(a, b, c) -> evalcousot9bbin(d - 1, c, c) [ 0 >= 0 /\ c >= 1 /\ c - 1 >= 0 /\ 2*c - 2 >= 0 /\ d >= 1 /\ d + c - 2 >= 0 /\ d - 1 >= 0 ]
	evalcousot9start(a, b, c) -> evalcousot9bbin(c - 3, c - 1, c) [ 0 >= 0 /\ c >= 1 /\ c - 1 >= 0 /\ 2*c - 2 >= 0 /\ 0 >= d /\ -d + c - 1 >= 0 /\ -d >= 0 /\ 1 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c - 2 >= 0 /\ 2*c - 4 >= 0 /\ c - 2 >= 1 /\ 2*c - 5 >= 0 /\ c - 3 >= 0 ]
We thus obtain the following problem:
25:	T:
		(1, 6)           evalcousot9start(a, b, c) -> evalcousot9bbin(d - 1, c, c) [ 0 >= 0 /\ c >= 1 /\ c - 1 >= 0 /\ 2*c - 2 >= 0 /\ d >= 1 /\ d + c - 2 >= 0 /\ d - 1 >= 0 ]
		(1, 15)          evalcousot9start(a, b, c) -> evalcousot9bbin(c - 3, c - 1, c) [ 0 >= 0 /\ c >= 1 /\ c - 1 >= 0 /\ 2*c - 2 >= 0 /\ 0 >= d /\ -d + c - 1 >= 0 /\ -d >= 0 /\ 1 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c - 2 >= 0 /\ 2*c - 4 >= 0 /\ c - 2 >= 1 /\ 2*c - 5 >= 0 /\ c - 3 >= 0 ]
		(?, 3)           evalcousot9bbin(a, b, c) -> evalcousot9bbin(a - 1, b, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ a >= 1 /\ a + c - 2 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= 1 ]
		(4*c + 2, 12)    evalcousot9bbin(a, b, c) -> evalcousot9bbin(c - 3, b - 1, c) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ b - 1 >= 0 /\ 0 >= a /\ -a + c - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ -b + c + 1 >= 0 /\ b - 1 >= 1 /\ b + c - 3 >= 0 /\ b - 2 >= 0 /\ c >= 1 /\ 2*c - 2 >= 0 /\ c + b - 3 >= 0 /\ c - 1 >= 1 /\ 2*c - 3 >= 0 /\ c + b - 4 >= 0 /\ c - 2 >= 0 /\ c - 2 >= 1 /\ 2*c - 4 >= 0 /\ c + b - 5 >= 0 /\ c - 3 >= 0 ]
	start location:	evalcousot9start
	leaf cost:	2

Complexity upper bound ?

Time: 2.645 sec (SMT: 2.461 sec)