YES(?, 49927*b + 5038821)

Initial complexity problem:
1:	T:
		(1, 1)    eval0(a, b, c, d) -> eval1(b, b, 1, d)
		(?, 1)    eval1(a, b, c, d) -> end(a, b, c, d) [ a >= 101 ]
		(?, 1)    eval1(a, b, c, d) -> eval3(a, b, c, d) [ 100 >= a ]
		(?, 1)    eval3(a, b, c, d) -> eval3(a + 11, b, c + 1, d) [ 100 >= a ]
		(?, 1)    eval3(a, b, c, d) -> eval5(a, b, c, d) [ a >= 101 ]
		(?, 1)    eval5(a, b, c, d) -> eval7(a - 10, b, c - 1, d) [ c >= 2 ]
		(?, 1)    eval7(a, b, c, d) -> eval5(a, b, c, a - 10) [ a >= 101 /\ c = 1 ]
		(?, 1)    eval7(a, b, c, d) -> eval9(a, b, c, d) [ 100 >= a ]
		(?, 1)    eval7(a, b, c, d) -> eval9(a, b, c, d) [ 2 >= c ]
		(?, 1)    eval7(a, b, c, d) -> eval9(a, b, c, d) [ c >= 0 ]
		(?, 1)    eval9(a, b, c, d) -> eval11(a - 10, b, c - 1, d) [ a >= 101 ]
		(?, 1)    eval9(a, b, c, d) -> eval11(a, b, c, d) [ 100 >= a ]
		(?, 1)    eval11(a, b, c, d) -> eval5(a + 11, b, c + 1, d)
	start location:	eval0
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c].
We thus obtain the following problem:
2:	T:
		(?, 1)    eval11(a, b, c) -> eval5(a + 11, b, c + 1)
		(?, 1)    eval9(a, b, c) -> eval11(a, b, c) [ 100 >= a ]
		(?, 1)    eval9(a, b, c) -> eval11(a - 10, b, c - 1) [ a >= 101 ]
		(?, 1)    eval7(a, b, c) -> eval9(a, b, c) [ c >= 0 ]
		(?, 1)    eval7(a, b, c) -> eval9(a, b, c) [ 2 >= c ]
		(?, 1)    eval7(a, b, c) -> eval9(a, b, c) [ 100 >= a ]
		(?, 1)    eval7(a, b, c) -> eval5(a, b, c) [ a >= 101 /\ c = 1 ]
		(?, 1)    eval5(a, b, c) -> eval7(a - 10, b, c - 1) [ c >= 2 ]
		(?, 1)    eval3(a, b, c) -> eval5(a, b, c) [ a >= 101 ]
		(?, 1)    eval3(a, b, c) -> eval3(a + 11, b, c + 1) [ 100 >= a ]
		(?, 1)    eval1(a, b, c) -> eval3(a, b, c) [ 100 >= a ]
		(?, 1)    eval1(a, b, c) -> end(a, b, c) [ a >= 101 ]
		(1, 1)    eval0(a, b, c) -> eval1(b, b, 1)
	start location:	eval0
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem:
3:	T:
		(?, 1)    eval11(a, b, c) -> eval5(a + 11, b, c + 1)
		(?, 1)    eval9(a, b, c) -> eval11(a, b, c) [ 100 >= a ]
		(?, 1)    eval9(a, b, c) -> eval11(a - 10, b, c - 1) [ a >= 101 ]
		(?, 1)    eval7(a, b, c) -> eval9(a, b, c) [ c >= 0 ]
		(?, 1)    eval7(a, b, c) -> eval9(a, b, c) [ 2 >= c ]
		(?, 1)    eval7(a, b, c) -> eval9(a, b, c) [ 100 >= a ]
		(?, 1)    eval5(a, b, c) -> eval7(a - 10, b, c - 1) [ c >= 2 ]
		(?, 1)    eval3(a, b, c) -> eval5(a, b, c) [ a >= 101 ]
		(?, 1)    eval3(a, b, c) -> eval3(a + 11, b, c + 1) [ 100 >= a ]
		(?, 1)    eval1(a, b, c) -> eval3(a, b, c) [ 100 >= a ]
		(1, 1)    eval0(a, b, c) -> eval1(b, b, 1)
	start location:	eval0
	leaf cost:	2

Repeatedly propagating knowledge in problem 3 produces the following problem:
4:	T:
		(?, 1)    eval11(a, b, c) -> eval5(a + 11, b, c + 1)
		(?, 1)    eval9(a, b, c) -> eval11(a, b, c) [ 100 >= a ]
		(?, 1)    eval9(a, b, c) -> eval11(a - 10, b, c - 1) [ a >= 101 ]
		(?, 1)    eval7(a, b, c) -> eval9(a, b, c) [ c >= 0 ]
		(?, 1)    eval7(a, b, c) -> eval9(a, b, c) [ 2 >= c ]
		(?, 1)    eval7(a, b, c) -> eval9(a, b, c) [ 100 >= a ]
		(?, 1)    eval5(a, b, c) -> eval7(a - 10, b, c - 1) [ c >= 2 ]
		(?, 1)    eval3(a, b, c) -> eval5(a, b, c) [ a >= 101 ]
		(?, 1)    eval3(a, b, c) -> eval3(a + 11, b, c + 1) [ 100 >= a ]
		(1, 1)    eval1(a, b, c) -> eval3(a, b, c) [ 100 >= a ]
		(1, 1)    eval0(a, b, c) -> eval1(b, b, 1)
	start location:	eval0
	leaf cost:	2

A polynomial rank function with
	Pol(eval11) = -101
	Pol(eval5) = -101
	Pol(eval9) = -101
	Pol(eval7) = -101
	Pol(eval3) = 100
	Pol(eval1) = 100
	Pol(eval0) = 100
orients all transitions weakly and the transition
	eval3(a, b, c) -> eval5(a, b, c) [ a >= 101 ]
strictly and produces the following problem:
5:	T:
		(?, 1)      eval11(a, b, c) -> eval5(a + 11, b, c + 1)
		(?, 1)      eval9(a, b, c) -> eval11(a, b, c) [ 100 >= a ]
		(?, 1)      eval9(a, b, c) -> eval11(a - 10, b, c - 1) [ a >= 101 ]
		(?, 1)      eval7(a, b, c) -> eval9(a, b, c) [ c >= 0 ]
		(?, 1)      eval7(a, b, c) -> eval9(a, b, c) [ 2 >= c ]
		(?, 1)      eval7(a, b, c) -> eval9(a, b, c) [ 100 >= a ]
		(?, 1)      eval5(a, b, c) -> eval7(a - 10, b, c - 1) [ c >= 2 ]
		(100, 1)    eval3(a, b, c) -> eval5(a, b, c) [ a >= 101 ]
		(?, 1)      eval3(a, b, c) -> eval3(a + 11, b, c + 1) [ 100 >= a ]
		(1, 1)      eval1(a, b, c) -> eval3(a, b, c) [ 100 >= a ]
		(1, 1)      eval0(a, b, c) -> eval1(b, b, 1)
	start location:	eval0
	leaf cost:	2

A polynomial rank function with
	Pol(eval9) = V_2
	Pol(eval11) = V_2
	Pol(eval7) = V_2
	Pol(eval5) = V_2
	Pol(eval3) = -V_1 + 101
and size complexities
	S("eval0(a, b, c) -> eval1(b, b, 1)", 0-0) = b
	S("eval0(a, b, c) -> eval1(b, b, 1)", 0-1) = b
	S("eval0(a, b, c) -> eval1(b, b, 1)", 0-2) = 1
	S("eval1(a, b, c) -> eval3(a, b, c) [ 100 >= a ]", 0-0) = b
	S("eval1(a, b, c) -> eval3(a, b, c) [ 100 >= a ]", 0-1) = b
	S("eval1(a, b, c) -> eval3(a, b, c) [ 100 >= a ]", 0-2) = 1
	S("eval3(a, b, c) -> eval3(a + 11, b, c + 1) [ 100 >= a ]", 0-0) = b + 111
	S("eval3(a, b, c) -> eval3(a + 11, b, c + 1) [ 100 >= a ]", 0-1) = b
	S("eval3(a, b, c) -> eval3(a + 11, b, c + 1) [ 100 >= a ]", 0-2) = ?
	S("eval3(a, b, c) -> eval5(a, b, c) [ a >= 101 ]", 0-0) = b + 111
	S("eval3(a, b, c) -> eval5(a, b, c) [ a >= 101 ]", 0-1) = b
	S("eval3(a, b, c) -> eval5(a, b, c) [ a >= 101 ]", 0-2) = ?
	S("eval5(a, b, c) -> eval7(a - 10, b, c - 1) [ c >= 2 ]", 0-0) = ?
	S("eval5(a, b, c) -> eval7(a - 10, b, c - 1) [ c >= 2 ]", 0-1) = b
	S("eval5(a, b, c) -> eval7(a - 10, b, c - 1) [ c >= 2 ]", 0-2) = ?
	S("eval7(a, b, c) -> eval9(a, b, c) [ 100 >= a ]", 0-0) = ?
	S("eval7(a, b, c) -> eval9(a, b, c) [ 100 >= a ]", 0-1) = b
	S("eval7(a, b, c) -> eval9(a, b, c) [ 100 >= a ]", 0-2) = ?
	S("eval7(a, b, c) -> eval9(a, b, c) [ 2 >= c ]", 0-0) = ?
	S("eval7(a, b, c) -> eval9(a, b, c) [ 2 >= c ]", 0-1) = b
	S("eval7(a, b, c) -> eval9(a, b, c) [ 2 >= c ]", 0-2) = ?
	S("eval7(a, b, c) -> eval9(a, b, c) [ c >= 0 ]", 0-0) = ?
	S("eval7(a, b, c) -> eval9(a, b, c) [ c >= 0 ]", 0-1) = b
	S("eval7(a, b, c) -> eval9(a, b, c) [ c >= 0 ]", 0-2) = ?
	S("eval9(a, b, c) -> eval11(a - 10, b, c - 1) [ a >= 101 ]", 0-0) = ?
	S("eval9(a, b, c) -> eval11(a - 10, b, c - 1) [ a >= 101 ]", 0-1) = b
	S("eval9(a, b, c) -> eval11(a - 10, b, c - 1) [ a >= 101 ]", 0-2) = ?
	S("eval9(a, b, c) -> eval11(a, b, c) [ 100 >= a ]", 0-0) = ?
	S("eval9(a, b, c) -> eval11(a, b, c) [ 100 >= a ]", 0-1) = b
	S("eval9(a, b, c) -> eval11(a, b, c) [ 100 >= a ]", 0-2) = ?
	S("eval11(a, b, c) -> eval5(a + 11, b, c + 1)", 0-0) = ?
	S("eval11(a, b, c) -> eval5(a + 11, b, c + 1)", 0-1) = b
	S("eval11(a, b, c) -> eval5(a + 11, b, c + 1)", 0-2) = ?
orients the transitions
	eval9(a, b, c) -> eval11(a, b, c) [ 100 >= a ]
	eval9(a, b, c) -> eval11(a - 10, b, c - 1) [ a >= 101 ]
	eval7(a, b, c) -> eval9(a, b, c) [ 100 >= a ]
	eval7(a, b, c) -> eval9(a, b, c) [ 2 >= c ]
	eval7(a, b, c) -> eval9(a, b, c) [ c >= 0 ]
	eval5(a, b, c) -> eval7(a - 10, b, c - 1) [ c >= 2 ]
	eval3(a, b, c) -> eval3(a + 11, b, c + 1) [ 100 >= a ]
	eval11(a, b, c) -> eval5(a + 11, b, c + 1)
weakly and the transition
	eval3(a, b, c) -> eval3(a + 11, b, c + 1) [ 100 >= a ]
strictly and produces the following problem:
6:	T:
		(?, 1)              eval11(a, b, c) -> eval5(a + 11, b, c + 1)
		(?, 1)              eval9(a, b, c) -> eval11(a, b, c) [ 100 >= a ]
		(?, 1)              eval9(a, b, c) -> eval11(a - 10, b, c - 1) [ a >= 101 ]
		(?, 1)              eval7(a, b, c) -> eval9(a, b, c) [ c >= 0 ]
		(?, 1)              eval7(a, b, c) -> eval9(a, b, c) [ 2 >= c ]
		(?, 1)              eval7(a, b, c) -> eval9(a, b, c) [ 100 >= a ]
		(?, 1)              eval5(a, b, c) -> eval7(a - 10, b, c - 1) [ c >= 2 ]
		(100, 1)            eval3(a, b, c) -> eval5(a, b, c) [ a >= 101 ]
		(101*b + 101, 1)    eval3(a, b, c) -> eval3(a + 11, b, c + 1) [ 100 >= a ]
		(1, 1)              eval1(a, b, c) -> eval3(a, b, c) [ 100 >= a ]
		(1, 1)              eval0(a, b, c) -> eval1(b, b, 1)
	start location:	eval0
	leaf cost:	2

Applied AI with 'oct' on problem 6 to obtain the following invariants:
  For symbol eval1: -X_3 + 1 >= 0 /\ X_3 - 1 >= 0 /\ X_1 - X_2 >= 0 /\ -X_1 + X_2 >= 0
  For symbol eval11: X_3 >= 0 /\ -X_2 + X_3 + 100 >= 0 /\ X_1 + X_3 - 91 >= 0 /\ -X_2 + 100 >= 0 /\ X_1 - X_2 + 9 >= 0 /\ X_1 - 91 >= 0
  For symbol eval3: X_3 - 1 >= 0 /\ -X_2 + X_3 + 99 >= 0 /\ -X_2 + 100 >= 0 /\ X_1 - X_2 >= 0
  For symbol eval5: X_3 - 1 >= 0 /\ -X_2 + X_3 + 99 >= 0 /\ X_1 + X_3 - 102 >= 0 /\ -X_2 + 100 >= 0 /\ X_1 - X_2 - 1 >= 0 /\ X_1 - 101 >= 0
  For symbol eval7: X_3 - 1 >= 0 /\ -X_2 + X_3 + 99 >= 0 /\ X_1 + X_3 - 92 >= 0 /\ -X_2 + 100 >= 0 /\ X_1 - X_2 + 9 >= 0 /\ X_1 - 91 >= 0
  For symbol eval9: X_3 - 1 >= 0 /\ -X_2 + X_3 + 99 >= 0 /\ X_1 + X_3 - 92 >= 0 /\ -X_2 + 100 >= 0 /\ X_1 - X_2 + 9 >= 0 /\ X_1 - 91 >= 0


This yielded the following problem:
7:	T:
		(1, 1)              eval0(a, b, c) -> eval1(b, b, 1)
		(1, 1)              eval1(a, b, c) -> eval3(a, b, c) [ -c + 1 >= 0 /\ c - 1 >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ 100 >= a ]
		(101*b + 101, 1)    eval3(a, b, c) -> eval3(a + 11, b, c + 1) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ -b + 100 >= 0 /\ a - b >= 0 /\ 100 >= a ]
		(100, 1)            eval3(a, b, c) -> eval5(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ -b + 100 >= 0 /\ a - b >= 0 /\ a >= 101 ]
		(?, 1)              eval5(a, b, c) -> eval7(a - 10, b, c - 1) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 102 >= 0 /\ -b + 100 >= 0 /\ a - b - 1 >= 0 /\ a - 101 >= 0 /\ c >= 2 ]
		(?, 1)              eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ 100 >= a ]
		(?, 1)              eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ 2 >= c ]
		(?, 1)              eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ c >= 0 ]
		(?, 1)              eval9(a, b, c) -> eval11(a - 10, b, c - 1) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ a >= 101 ]
		(?, 1)              eval9(a, b, c) -> eval11(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ 100 >= a ]
		(?, 1)              eval11(a, b, c) -> eval5(a + 11, b, c + 1) [ c >= 0 /\ -b + c + 100 >= 0 /\ a + c - 91 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 ]
	start location:	eval0
	leaf cost:	2

A polynomial rank function with
	Pol(eval0) = -132*V_2 + 13072
	Pol(eval1) = -132*V_1 + 1452*V_3 + 11620
	Pol(eval3) = -132*V_1 + 1452*V_3 + 11620
	Pol(eval5) = -132*V_1 + 1452*V_3 + 11620
	Pol(eval7) = -132*V_1 + 1452*V_3 + 11751
	Pol(eval9) = -132*V_1 + 1452*V_3 + 11622
	Pol(eval11) = -132*V_1 + 1452*V_3 + 11621
orients all transitions weakly and the transition
	eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ 100 >= a ]
strictly and produces the following problem:
8:	T:
		(1, 1)                eval0(a, b, c) -> eval1(b, b, 1)
		(1, 1)                eval1(a, b, c) -> eval3(a, b, c) [ -c + 1 >= 0 /\ c - 1 >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ 100 >= a ]
		(101*b + 101, 1)      eval3(a, b, c) -> eval3(a + 11, b, c + 1) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ -b + 100 >= 0 /\ a - b >= 0 /\ 100 >= a ]
		(100, 1)              eval3(a, b, c) -> eval5(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ -b + 100 >= 0 /\ a - b >= 0 /\ a >= 101 ]
		(?, 1)                eval5(a, b, c) -> eval7(a - 10, b, c - 1) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 102 >= 0 /\ -b + 100 >= 0 /\ a - b - 1 >= 0 /\ a - 101 >= 0 /\ c >= 2 ]
		(132*b + 13072, 1)    eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ 100 >= a ]
		(?, 1)                eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ 2 >= c ]
		(?, 1)                eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ c >= 0 ]
		(?, 1)                eval9(a, b, c) -> eval11(a - 10, b, c - 1) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ a >= 101 ]
		(?, 1)                eval9(a, b, c) -> eval11(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ 100 >= a ]
		(?, 1)                eval11(a, b, c) -> eval5(a + 11, b, c + 1) [ c >= 0 /\ -b + c + 100 >= 0 /\ a + c - 91 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 ]
	start location:	eval0
	leaf cost:	2

A polynomial rank function with
	Pol(eval0) = -54*V_2 + 5404
	Pol(eval1) = -5*V_1 - 49*V_2 + 50*V_3 + 5354
	Pol(eval3) = -5*V_1 - 49*V_2 + 50*V_3 + 5354
	Pol(eval5) = -5*V_1 - 49*V_2 + 50*V_3 + 5354
	Pol(eval7) = -5*V_1 - 49*V_2 + 50*V_3 + 5352
	Pol(eval9) = -5*V_1 - 49*V_2 + 50*V_3 + 5351
	Pol(eval11) = -5*V_1 - 49*V_2 + 50*V_3 + 5350
orients all transitions weakly and the transition
	eval9(a, b, c) -> eval11(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ 100 >= a ]
strictly and produces the following problem:
9:	T:
		(1, 1)                eval0(a, b, c) -> eval1(b, b, 1)
		(1, 1)                eval1(a, b, c) -> eval3(a, b, c) [ -c + 1 >= 0 /\ c - 1 >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ 100 >= a ]
		(101*b + 101, 1)      eval3(a, b, c) -> eval3(a + 11, b, c + 1) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ -b + 100 >= 0 /\ a - b >= 0 /\ 100 >= a ]
		(100, 1)              eval3(a, b, c) -> eval5(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ -b + 100 >= 0 /\ a - b >= 0 /\ a >= 101 ]
		(?, 1)                eval5(a, b, c) -> eval7(a - 10, b, c - 1) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 102 >= 0 /\ -b + 100 >= 0 /\ a - b - 1 >= 0 /\ a - 101 >= 0 /\ c >= 2 ]
		(132*b + 13072, 1)    eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ 100 >= a ]
		(?, 1)                eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ 2 >= c ]
		(?, 1)                eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ c >= 0 ]
		(?, 1)                eval9(a, b, c) -> eval11(a - 10, b, c - 1) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ a >= 101 ]
		(54*b + 5404, 1)      eval9(a, b, c) -> eval11(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ 100 >= a ]
		(?, 1)                eval11(a, b, c) -> eval5(a + 11, b, c + 1) [ c >= 0 /\ -b + c + 100 >= 0 /\ a + c - 91 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 ]
	start location:	eval0
	leaf cost:	2

A polynomial rank function with
	Pol(eval9) = V_1 - 91
	Pol(eval11) = V_1 - 82
	Pol(eval7) = V_1 - 90
	Pol(eval5) = V_1 - 94
and size complexities
	S("eval11(a, b, c) -> eval5(a + 11, b, c + 1) [ c >= 0 /\\ -b + c + 100 >= 0 /\\ a + c - 91 >= 0 /\\ -b + 100 >= 0 /\\ a - b + 9 >= 0 /\\ a - 91 >= 0 ]", 0-0) = ?
	S("eval11(a, b, c) -> eval5(a + 11, b, c + 1) [ c >= 0 /\\ -b + c + 100 >= 0 /\\ a + c - 91 >= 0 /\\ -b + 100 >= 0 /\\ a - b + 9 >= 0 /\\ a - 91 >= 0 ]", 0-1) = b
	S("eval11(a, b, c) -> eval5(a + 11, b, c + 1) [ c >= 0 /\\ -b + c + 100 >= 0 /\\ a + c - 91 >= 0 /\\ -b + 100 >= 0 /\\ a - b + 9 >= 0 /\\ a - 91 >= 0 ]", 0-2) = ?
	S("eval9(a, b, c) -> eval11(a, b, c) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ a + c - 92 >= 0 /\\ -b + 100 >= 0 /\\ a - b + 9 >= 0 /\\ a - 91 >= 0 /\\ 100 >= a ]", 0-0) = 100
	S("eval9(a, b, c) -> eval11(a, b, c) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ a + c - 92 >= 0 /\\ -b + 100 >= 0 /\\ a - b + 9 >= 0 /\\ a - 91 >= 0 /\\ 100 >= a ]", 0-1) = b
	S("eval9(a, b, c) -> eval11(a, b, c) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ a + c - 92 >= 0 /\\ -b + 100 >= 0 /\\ a - b + 9 >= 0 /\\ a - 91 >= 0 /\\ 100 >= a ]", 0-2) = ?
	S("eval9(a, b, c) -> eval11(a - 10, b, c - 1) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ a + c - 92 >= 0 /\\ -b + 100 >= 0 /\\ a - b + 9 >= 0 /\\ a - 91 >= 0 /\\ a >= 101 ]", 0-0) = ?
	S("eval9(a, b, c) -> eval11(a - 10, b, c - 1) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ a + c - 92 >= 0 /\\ -b + 100 >= 0 /\\ a - b + 9 >= 0 /\\ a - 91 >= 0 /\\ a >= 101 ]", 0-1) = b
	S("eval9(a, b, c) -> eval11(a - 10, b, c - 1) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ a + c - 92 >= 0 /\\ -b + 100 >= 0 /\\ a - b + 9 >= 0 /\\ a - 91 >= 0 /\\ a >= 101 ]", 0-2) = ?
	S("eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ a + c - 92 >= 0 /\\ -b + 100 >= 0 /\\ a - b + 9 >= 0 /\\ a - 91 >= 0 /\\ c >= 0 ]", 0-0) = ?
	S("eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ a + c - 92 >= 0 /\\ -b + 100 >= 0 /\\ a - b + 9 >= 0 /\\ a - 91 >= 0 /\\ c >= 0 ]", 0-1) = b
	S("eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ a + c - 92 >= 0 /\\ -b + 100 >= 0 /\\ a - b + 9 >= 0 /\\ a - 91 >= 0 /\\ c >= 0 ]", 0-2) = ?
	S("eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ a + c - 92 >= 0 /\\ -b + 100 >= 0 /\\ a - b + 9 >= 0 /\\ a - 91 >= 0 /\\ 2 >= c ]", 0-0) = ?
	S("eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ a + c - 92 >= 0 /\\ -b + 100 >= 0 /\\ a - b + 9 >= 0 /\\ a - 91 >= 0 /\\ 2 >= c ]", 0-1) = b
	S("eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ a + c - 92 >= 0 /\\ -b + 100 >= 0 /\\ a - b + 9 >= 0 /\\ a - 91 >= 0 /\\ 2 >= c ]", 0-2) = 2
	S("eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ a + c - 92 >= 0 /\\ -b + 100 >= 0 /\\ a - b + 9 >= 0 /\\ a - 91 >= 0 /\\ 100 >= a ]", 0-0) = 100
	S("eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ a + c - 92 >= 0 /\\ -b + 100 >= 0 /\\ a - b + 9 >= 0 /\\ a - 91 >= 0 /\\ 100 >= a ]", 0-1) = b
	S("eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ a + c - 92 >= 0 /\\ -b + 100 >= 0 /\\ a - b + 9 >= 0 /\\ a - 91 >= 0 /\\ 100 >= a ]", 0-2) = ?
	S("eval5(a, b, c) -> eval7(a - 10, b, c - 1) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ a + c - 102 >= 0 /\\ -b + 100 >= 0 /\\ a - b - 1 >= 0 /\\ a - 101 >= 0 /\\ c >= 2 ]", 0-0) = ?
	S("eval5(a, b, c) -> eval7(a - 10, b, c - 1) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ a + c - 102 >= 0 /\\ -b + 100 >= 0 /\\ a - b - 1 >= 0 /\\ a - 101 >= 0 /\\ c >= 2 ]", 0-1) = b
	S("eval5(a, b, c) -> eval7(a - 10, b, c - 1) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ a + c - 102 >= 0 /\\ -b + 100 >= 0 /\\ a - b - 1 >= 0 /\\ a - 101 >= 0 /\\ c >= 2 ]", 0-2) = ?
	S("eval3(a, b, c) -> eval5(a, b, c) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ -b + 100 >= 0 /\\ a - b >= 0 /\\ a >= 101 ]", 0-0) = b + 111
	S("eval3(a, b, c) -> eval5(a, b, c) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ -b + 100 >= 0 /\\ a - b >= 0 /\\ a >= 101 ]", 0-1) = b
	S("eval3(a, b, c) -> eval5(a, b, c) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ -b + 100 >= 0 /\\ a - b >= 0 /\\ a >= 101 ]", 0-2) = 101*b + 105090702
	S("eval3(a, b, c) -> eval3(a + 11, b, c + 1) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ -b + 100 >= 0 /\\ a - b >= 0 /\\ 100 >= a ]", 0-0) = b + 111
	S("eval3(a, b, c) -> eval3(a + 11, b, c + 1) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ -b + 100 >= 0 /\\ a - b >= 0 /\\ 100 >= a ]", 0-1) = b
	S("eval3(a, b, c) -> eval3(a + 11, b, c + 1) [ c - 1 >= 0 /\\ -b + c + 99 >= 0 /\\ -b + 100 >= 0 /\\ a - b >= 0 /\\ 100 >= a ]", 0-2) = 101*b + 1040502
	S("eval1(a, b, c) -> eval3(a, b, c) [ -c + 1 >= 0 /\\ c - 1 >= 0 /\\ a - b >= 0 /\\ -a + b >= 0 /\\ 100 >= a ]", 0-0) = b
	S("eval1(a, b, c) -> eval3(a, b, c) [ -c + 1 >= 0 /\\ c - 1 >= 0 /\\ a - b >= 0 /\\ -a + b >= 0 /\\ 100 >= a ]", 0-1) = b
	S("eval1(a, b, c) -> eval3(a, b, c) [ -c + 1 >= 0 /\\ c - 1 >= 0 /\\ a - b >= 0 /\\ -a + b >= 0 /\\ 100 >= a ]", 0-2) = 1
	S("eval0(a, b, c) -> eval1(b, b, 1)", 0-0) = b
	S("eval0(a, b, c) -> eval1(b, b, 1)", 0-1) = b
	S("eval0(a, b, c) -> eval1(b, b, 1)", 0-2) = 1
orients the transitions
	eval9(a, b, c) -> eval11(a - 10, b, c - 1) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ a >= 101 ]
	eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ 2 >= c ]
	eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ c >= 0 ]
	eval5(a, b, c) -> eval7(a - 10, b, c - 1) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 102 >= 0 /\ -b + 100 >= 0 /\ a - b - 1 >= 0 /\ a - 101 >= 0 /\ c >= 2 ]
	eval11(a, b, c) -> eval5(a + 11, b, c + 1) [ c >= 0 /\ -b + c + 100 >= 0 /\ a + c - 91 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 ]
weakly and the transitions
	eval9(a, b, c) -> eval11(a - 10, b, c - 1) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ a >= 101 ]
	eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ 2 >= c ]
	eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ c >= 0 ]
	eval5(a, b, c) -> eval7(a - 10, b, c - 1) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 102 >= 0 /\ -b + 100 >= 0 /\ a - b - 1 >= 0 /\ a - 101 >= 0 /\ c >= 2 ]
	eval11(a, b, c) -> eval5(a + 11, b, c + 1) [ c >= 0 /\ -b + c + 100 >= 0 /\ a + c - 91 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 ]
strictly and produces the following problem:
10:	T:
		(1, 1)                   eval0(a, b, c) -> eval1(b, b, 1)
		(1, 1)                   eval1(a, b, c) -> eval3(a, b, c) [ -c + 1 >= 0 /\ c - 1 >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ 100 >= a ]
		(101*b + 101, 1)         eval3(a, b, c) -> eval3(a + 11, b, c + 1) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ -b + 100 >= 0 /\ a - b >= 0 /\ 100 >= a ]
		(100, 1)                 eval3(a, b, c) -> eval5(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ -b + 100 >= 0 /\ a - b >= 0 /\ a >= 101 ]
		(9928*b + 1004028, 1)    eval5(a, b, c) -> eval7(a - 10, b, c - 1) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 102 >= 0 /\ -b + 100 >= 0 /\ a - b - 1 >= 0 /\ a - 101 >= 0 /\ c >= 2 ]
		(132*b + 13072, 1)       eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ 100 >= a ]
		(9928*b + 1004028, 1)    eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ 2 >= c ]
		(9928*b + 1004028, 1)    eval7(a, b, c) -> eval9(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ c >= 0 ]
		(9928*b + 1004028, 1)    eval9(a, b, c) -> eval11(a - 10, b, c - 1) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ a >= 101 ]
		(54*b + 5404, 1)         eval9(a, b, c) -> eval11(a, b, c) [ c - 1 >= 0 /\ -b + c + 99 >= 0 /\ a + c - 92 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 /\ 100 >= a ]
		(9928*b + 1004028, 1)    eval11(a, b, c) -> eval5(a + 11, b, c + 1) [ c >= 0 /\ -b + c + 100 >= 0 /\ a + c - 91 >= 0 /\ -b + 100 >= 0 /\ a - b + 9 >= 0 /\ a - 91 >= 0 ]
	start location:	eval0
	leaf cost:	2

Complexity upper bound 49927*b + 5038821

Time: 1.045 sec (SMT: 0.984 sec)