YES(?, 27608*a + 135*a^2 + 1410294)

Initial complexity problem:
1:	T:
		(1, 1)    evalsipma91start(a, b, c, d) -> evalsipma91entryin(a, b, c, d)
		(?, 1)    evalsipma91entryin(a, b, c, d) -> evalsipma91returnin(a, b, c, d) [ a >= 101 ]
		(?, 1)    evalsipma91entryin(a, b, c, d) -> evalsipma91bb3in(1, a, c, d) [ 100 >= a ]
		(?, 1)    evalsipma91bb3in(a, b, c, d) -> evalsipma91bb2in(a, b, c, d) [ 100 >= b ]
		(?, 1)    evalsipma91bb3in(a, b, c, d) -> evalsipma91bb11in(a, b, c, d) [ b >= 101 ]
		(?, 1)    evalsipma91bb2in(a, b, c, d) -> evalsipma91bb3in(a + 1, b + 11, c, d)
		(?, 1)    evalsipma91bb11in(a, b, c, d) -> evalsipma91bb5in(a, b, c, d) [ a >= 2 ]
		(?, 1)    evalsipma91bb11in(a, b, c, d) -> evalsipma91returnin(a, b, c, d) [ 1 >= a ]
		(?, 1)    evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ 110 >= b ]
		(?, 1)    evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ 1 >= a ]
		(?, 1)    evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ a >= 3 ]
		(?, 1)    evalsipma91bb5in(a, b, c, d) -> evalsipma91bb11in(a - 1, b - 10, c, d) [ b >= 111 /\ a = 2 ]
		(?, 1)    evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 1, c, d) [ c >= 101 ]
		(?, 1)    evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 11, c, d) [ c >= 101 /\ 100 >= c ]
		(?, 1)    evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d + 1, c + 1, c, d) [ 100 >= c /\ c >= 101 ]
		(?, 1)    evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d + 1, c + 11, c, d) [ 100 >= c ]
		(?, 1)    evalsipma91returnin(a, b, c, d) -> evalsipma91stop(a, b, c, d)
	start location:	evalsipma91start
	leaf cost:	0

Testing for unsatisfiable constraints removes the following transitions from problem 1:
	evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 11, c, d) [ c >= 101 /\ 100 >= c ]
	evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d + 1, c + 1, c, d) [ 100 >= c /\ c >= 101 ]
We thus obtain the following problem:
2:	T:
		(1, 1)    evalsipma91start(a, b, c, d) -> evalsipma91entryin(a, b, c, d)
		(?, 1)    evalsipma91entryin(a, b, c, d) -> evalsipma91returnin(a, b, c, d) [ a >= 101 ]
		(?, 1)    evalsipma91entryin(a, b, c, d) -> evalsipma91bb3in(1, a, c, d) [ 100 >= a ]
		(?, 1)    evalsipma91bb3in(a, b, c, d) -> evalsipma91bb2in(a, b, c, d) [ 100 >= b ]
		(?, 1)    evalsipma91bb3in(a, b, c, d) -> evalsipma91bb11in(a, b, c, d) [ b >= 101 ]
		(?, 1)    evalsipma91bb2in(a, b, c, d) -> evalsipma91bb3in(a + 1, b + 11, c, d)
		(?, 1)    evalsipma91bb11in(a, b, c, d) -> evalsipma91bb5in(a, b, c, d) [ a >= 2 ]
		(?, 1)    evalsipma91bb11in(a, b, c, d) -> evalsipma91returnin(a, b, c, d) [ 1 >= a ]
		(?, 1)    evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ 110 >= b ]
		(?, 1)    evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ 1 >= a ]
		(?, 1)    evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ a >= 3 ]
		(?, 1)    evalsipma91bb5in(a, b, c, d) -> evalsipma91bb11in(a - 1, b - 10, c, d) [ b >= 111 /\ a = 2 ]
		(?, 1)    evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 1, c, d) [ c >= 101 ]
		(?, 1)    evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d + 1, c + 11, c, d) [ 100 >= c ]
		(?, 1)    evalsipma91returnin(a, b, c, d) -> evalsipma91stop(a, b, c, d)
	start location:	evalsipma91start
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalsipma91start(a, b, c, d) -> evalsipma91entryin(a, b, c, d)
		(?, 1)    evalsipma91entryin(a, b, c, d) -> evalsipma91bb3in(1, a, c, d) [ 100 >= a ]
		(?, 1)    evalsipma91bb3in(a, b, c, d) -> evalsipma91bb2in(a, b, c, d) [ 100 >= b ]
		(?, 1)    evalsipma91bb3in(a, b, c, d) -> evalsipma91bb11in(a, b, c, d) [ b >= 101 ]
		(?, 1)    evalsipma91bb2in(a, b, c, d) -> evalsipma91bb3in(a + 1, b + 11, c, d)
		(?, 1)    evalsipma91bb11in(a, b, c, d) -> evalsipma91bb5in(a, b, c, d) [ a >= 2 ]
		(?, 1)    evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ 110 >= b ]
		(?, 1)    evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ 1 >= a ]
		(?, 1)    evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ a >= 3 ]
		(?, 1)    evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 1, c, d) [ c >= 101 ]
		(?, 1)    evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d + 1, c + 11, c, d) [ 100 >= c ]
	start location:	evalsipma91start
	leaf cost:	4

Testing for reachability in the complexity graph removes the following transition from problem 3:
	evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ 1 >= a ]
We thus obtain the following problem:
4:	T:
		(?, 1)    evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 1, c, d) [ c >= 101 ]
		(?, 1)    evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d + 1, c + 11, c, d) [ 100 >= c ]
		(?, 1)    evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ a >= 3 ]
		(?, 1)    evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ 110 >= b ]
		(?, 1)    evalsipma91bb11in(a, b, c, d) -> evalsipma91bb5in(a, b, c, d) [ a >= 2 ]
		(?, 1)    evalsipma91bb3in(a, b, c, d) -> evalsipma91bb11in(a, b, c, d) [ b >= 101 ]
		(?, 1)    evalsipma91bb2in(a, b, c, d) -> evalsipma91bb3in(a + 1, b + 11, c, d)
		(?, 1)    evalsipma91bb3in(a, b, c, d) -> evalsipma91bb2in(a, b, c, d) [ 100 >= b ]
		(?, 1)    evalsipma91entryin(a, b, c, d) -> evalsipma91bb3in(1, a, c, d) [ 100 >= a ]
		(1, 1)    evalsipma91start(a, b, c, d) -> evalsipma91entryin(a, b, c, d)
	start location:	evalsipma91start
	leaf cost:	4

Repeatedly propagating knowledge in problem 4 produces the following problem:
5:	T:
		(?, 1)    evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 1, c, d) [ c >= 101 ]
		(?, 1)    evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d + 1, c + 11, c, d) [ 100 >= c ]
		(?, 1)    evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ a >= 3 ]
		(?, 1)    evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ 110 >= b ]
		(?, 1)    evalsipma91bb11in(a, b, c, d) -> evalsipma91bb5in(a, b, c, d) [ a >= 2 ]
		(?, 1)    evalsipma91bb3in(a, b, c, d) -> evalsipma91bb11in(a, b, c, d) [ b >= 101 ]
		(?, 1)    evalsipma91bb2in(a, b, c, d) -> evalsipma91bb3in(a + 1, b + 11, c, d)
		(?, 1)    evalsipma91bb3in(a, b, c, d) -> evalsipma91bb2in(a, b, c, d) [ 100 >= b ]
		(1, 1)    evalsipma91entryin(a, b, c, d) -> evalsipma91bb3in(1, a, c, d) [ 100 >= a ]
		(1, 1)    evalsipma91start(a, b, c, d) -> evalsipma91entryin(a, b, c, d)
	start location:	evalsipma91start
	leaf cost:	4

A polynomial rank function with
	Pol(evalsipma91bb8in) = -101
	Pol(evalsipma91bb11in) = -101
	Pol(evalsipma91bb5in) = -101
	Pol(evalsipma91bb3in) = 1
	Pol(evalsipma91bb2in) = 1
	Pol(evalsipma91entryin) = 1
	Pol(evalsipma91start) = 1
orients all transitions weakly and the transition
	evalsipma91bb3in(a, b, c, d) -> evalsipma91bb11in(a, b, c, d) [ b >= 101 ]
strictly and produces the following problem:
6:	T:
		(?, 1)    evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 1, c, d) [ c >= 101 ]
		(?, 1)    evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d + 1, c + 11, c, d) [ 100 >= c ]
		(?, 1)    evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ a >= 3 ]
		(?, 1)    evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ 110 >= b ]
		(?, 1)    evalsipma91bb11in(a, b, c, d) -> evalsipma91bb5in(a, b, c, d) [ a >= 2 ]
		(1, 1)    evalsipma91bb3in(a, b, c, d) -> evalsipma91bb11in(a, b, c, d) [ b >= 101 ]
		(?, 1)    evalsipma91bb2in(a, b, c, d) -> evalsipma91bb3in(a + 1, b + 11, c, d)
		(?, 1)    evalsipma91bb3in(a, b, c, d) -> evalsipma91bb2in(a, b, c, d) [ 100 >= b ]
		(1, 1)    evalsipma91entryin(a, b, c, d) -> evalsipma91bb3in(1, a, c, d) [ 100 >= a ]
		(1, 1)    evalsipma91start(a, b, c, d) -> evalsipma91entryin(a, b, c, d)
	start location:	evalsipma91start
	leaf cost:	4

A polynomial rank function with
	Pol(evalsipma91bb8in) = 2
	Pol(evalsipma91bb11in) = 2
	Pol(evalsipma91bb5in) = 2
	Pol(evalsipma91bb3in) = -V_2 + 101
	Pol(evalsipma91bb2in) = -V_2 + 91
and size complexities
	S("evalsipma91start(a, b, c, d) -> evalsipma91entryin(a, b, c, d)", 0-0) = a
	S("evalsipma91start(a, b, c, d) -> evalsipma91entryin(a, b, c, d)", 0-1) = b
	S("evalsipma91start(a, b, c, d) -> evalsipma91entryin(a, b, c, d)", 0-2) = c
	S("evalsipma91start(a, b, c, d) -> evalsipma91entryin(a, b, c, d)", 0-3) = d
	S("evalsipma91entryin(a, b, c, d) -> evalsipma91bb3in(1, a, c, d) [ 100 >= a ]", 0-0) = 1
	S("evalsipma91entryin(a, b, c, d) -> evalsipma91bb3in(1, a, c, d) [ 100 >= a ]", 0-1) = a
	S("evalsipma91entryin(a, b, c, d) -> evalsipma91bb3in(1, a, c, d) [ 100 >= a ]", 0-2) = c
	S("evalsipma91entryin(a, b, c, d) -> evalsipma91bb3in(1, a, c, d) [ 100 >= a ]", 0-3) = d
	S("evalsipma91bb3in(a, b, c, d) -> evalsipma91bb2in(a, b, c, d) [ 100 >= b ]", 0-0) = ?
	S("evalsipma91bb3in(a, b, c, d) -> evalsipma91bb2in(a, b, c, d) [ 100 >= b ]", 0-1) = ?
	S("evalsipma91bb3in(a, b, c, d) -> evalsipma91bb2in(a, b, c, d) [ 100 >= b ]", 0-2) = c
	S("evalsipma91bb3in(a, b, c, d) -> evalsipma91bb2in(a, b, c, d) [ 100 >= b ]", 0-3) = d
	S("evalsipma91bb2in(a, b, c, d) -> evalsipma91bb3in(a + 1, b + 11, c, d)", 0-0) = ?
	S("evalsipma91bb2in(a, b, c, d) -> evalsipma91bb3in(a + 1, b + 11, c, d)", 0-1) = ?
	S("evalsipma91bb2in(a, b, c, d) -> evalsipma91bb3in(a + 1, b + 11, c, d)", 0-2) = c
	S("evalsipma91bb2in(a, b, c, d) -> evalsipma91bb3in(a + 1, b + 11, c, d)", 0-3) = d
	S("evalsipma91bb3in(a, b, c, d) -> evalsipma91bb11in(a, b, c, d) [ b >= 101 ]", 0-0) = ?
	S("evalsipma91bb3in(a, b, c, d) -> evalsipma91bb11in(a, b, c, d) [ b >= 101 ]", 0-1) = ?
	S("evalsipma91bb3in(a, b, c, d) -> evalsipma91bb11in(a, b, c, d) [ b >= 101 ]", 0-2) = c
	S("evalsipma91bb3in(a, b, c, d) -> evalsipma91bb11in(a, b, c, d) [ b >= 101 ]", 0-3) = d
	S("evalsipma91bb11in(a, b, c, d) -> evalsipma91bb5in(a, b, c, d) [ a >= 2 ]", 0-0) = ?
	S("evalsipma91bb11in(a, b, c, d) -> evalsipma91bb5in(a, b, c, d) [ a >= 2 ]", 0-1) = ?
	S("evalsipma91bb11in(a, b, c, d) -> evalsipma91bb5in(a, b, c, d) [ a >= 2 ]", 0-2) = ?
	S("evalsipma91bb11in(a, b, c, d) -> evalsipma91bb5in(a, b, c, d) [ a >= 2 ]", 0-3) = ?
	S("evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ 110 >= b ]", 0-0) = ?
	S("evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ 110 >= b ]", 0-1) = ?
	S("evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ 110 >= b ]", 0-2) = ?
	S("evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ 110 >= b ]", 0-3) = ?
	S("evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ a >= 3 ]", 0-0) = ?
	S("evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ a >= 3 ]", 0-1) = ?
	S("evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ a >= 3 ]", 0-2) = ?
	S("evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ a >= 3 ]", 0-3) = ?
	S("evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d + 1, c + 11, c, d) [ 100 >= c ]", 0-0) = ?
	S("evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d + 1, c + 11, c, d) [ 100 >= c ]", 0-1) = ?
	S("evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d + 1, c + 11, c, d) [ 100 >= c ]", 0-2) = ?
	S("evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d + 1, c + 11, c, d) [ 100 >= c ]", 0-3) = ?
	S("evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 1, c, d) [ c >= 101 ]", 0-0) = ?
	S("evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 1, c, d) [ c >= 101 ]", 0-1) = ?
	S("evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 1, c, d) [ c >= 101 ]", 0-2) = ?
	S("evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 1, c, d) [ c >= 101 ]", 0-3) = ?
orients the transitions
	evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d + 1, c + 11, c, d) [ 100 >= c ]
	evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 1, c, d) [ c >= 101 ]
	evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ 110 >= b ]
	evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ a >= 3 ]
	evalsipma91bb3in(a, b, c, d) -> evalsipma91bb2in(a, b, c, d) [ 100 >= b ]
	evalsipma91bb2in(a, b, c, d) -> evalsipma91bb3in(a + 1, b + 11, c, d)
	evalsipma91bb11in(a, b, c, d) -> evalsipma91bb5in(a, b, c, d) [ a >= 2 ]
weakly and the transition
	evalsipma91bb3in(a, b, c, d) -> evalsipma91bb2in(a, b, c, d) [ 100 >= b ]
strictly and produces the following problem:
7:	T:
		(?, 1)          evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 1, c, d) [ c >= 101 ]
		(?, 1)          evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d + 1, c + 11, c, d) [ 100 >= c ]
		(?, 1)          evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ a >= 3 ]
		(?, 1)          evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ 110 >= b ]
		(?, 1)          evalsipma91bb11in(a, b, c, d) -> evalsipma91bb5in(a, b, c, d) [ a >= 2 ]
		(1, 1)          evalsipma91bb3in(a, b, c, d) -> evalsipma91bb11in(a, b, c, d) [ b >= 101 ]
		(?, 1)          evalsipma91bb2in(a, b, c, d) -> evalsipma91bb3in(a + 1, b + 11, c, d)
		(a + 103, 1)    evalsipma91bb3in(a, b, c, d) -> evalsipma91bb2in(a, b, c, d) [ 100 >= b ]
		(1, 1)          evalsipma91entryin(a, b, c, d) -> evalsipma91bb3in(1, a, c, d) [ 100 >= a ]
		(1, 1)          evalsipma91start(a, b, c, d) -> evalsipma91entryin(a, b, c, d)
	start location:	evalsipma91start
	leaf cost:	4

Repeatedly propagating knowledge in problem 7 produces the following problem:
8:	T:
		(?, 1)          evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 1, c, d) [ c >= 101 ]
		(?, 1)          evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d + 1, c + 11, c, d) [ 100 >= c ]
		(?, 1)          evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ a >= 3 ]
		(?, 1)          evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ 110 >= b ]
		(?, 1)          evalsipma91bb11in(a, b, c, d) -> evalsipma91bb5in(a, b, c, d) [ a >= 2 ]
		(1, 1)          evalsipma91bb3in(a, b, c, d) -> evalsipma91bb11in(a, b, c, d) [ b >= 101 ]
		(a + 103, 1)    evalsipma91bb2in(a, b, c, d) -> evalsipma91bb3in(a + 1, b + 11, c, d)
		(a + 103, 1)    evalsipma91bb3in(a, b, c, d) -> evalsipma91bb2in(a, b, c, d) [ 100 >= b ]
		(1, 1)          evalsipma91entryin(a, b, c, d) -> evalsipma91bb3in(1, a, c, d) [ 100 >= a ]
		(1, 1)          evalsipma91start(a, b, c, d) -> evalsipma91entryin(a, b, c, d)
	start location:	evalsipma91start
	leaf cost:	4

Applied AI with 'oct' on problem 8 to obtain the following invariants:
  For symbol evalsipma91bb11in: X_2 - 101 >= 0 /\ X_1 + X_2 - 102 >= 0 /\ X_1 - 1 >= 0
  For symbol evalsipma91bb2in: -X_2 + 100 >= 0 /\ X_1 - X_2 + 99 >= 0 /\ X_1 - 1 >= 0
  For symbol evalsipma91bb3in: X_1 - 1 >= 0
  For symbol evalsipma91bb5in: X_2 - 101 >= 0 /\ X_1 + X_2 - 103 >= 0 /\ X_1 - 2 >= 0
  For symbol evalsipma91bb8in: X_1 - X_4 - 1 >= 0 /\ X_4 - 1 >= 0 /\ X_3 + X_4 - 92 >= 0 /\ X_2 + X_4 - 102 >= 0 /\ X_1 + X_4 - 3 >= 0 /\ -X_1 + X_4 + 1 >= 0 /\ X_2 - X_3 - 10 >= 0 /\ X_3 - 91 >= 0 /\ X_2 + X_3 - 192 >= 0 /\ -X_2 + X_3 + 10 >= 0 /\ X_1 + X_3 - 93 >= 0 /\ X_2 - 101 >= 0 /\ X_1 + X_2 - 103 >= 0 /\ X_1 - 2 >= 0


This yielded the following problem:
9:	T:
		(1, 1)          evalsipma91start(a, b, c, d) -> evalsipma91entryin(a, b, c, d)
		(1, 1)          evalsipma91entryin(a, b, c, d) -> evalsipma91bb3in(1, a, c, d) [ 100 >= a ]
		(a + 103, 1)    evalsipma91bb3in(a, b, c, d) -> evalsipma91bb2in(a, b, c, d) [ a - 1 >= 0 /\ 100 >= b ]
		(a + 103, 1)    evalsipma91bb2in(a, b, c, d) -> evalsipma91bb3in(a + 1, b + 11, c, d) [ -b + 100 >= 0 /\ a - b + 99 >= 0 /\ a - 1 >= 0 ]
		(1, 1)          evalsipma91bb3in(a, b, c, d) -> evalsipma91bb11in(a, b, c, d) [ a - 1 >= 0 /\ b >= 101 ]
		(?, 1)          evalsipma91bb11in(a, b, c, d) -> evalsipma91bb5in(a, b, c, d) [ b - 101 >= 0 /\ a + b - 102 >= 0 /\ a - 1 >= 0 /\ a >= 2 ]
		(?, 1)          evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ b - 101 >= 0 /\ a + b - 103 >= 0 /\ a - 2 >= 0 /\ 110 >= b ]
		(?, 1)          evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ b - 101 >= 0 /\ a + b - 103 >= 0 /\ a - 2 >= 0 /\ a >= 3 ]
		(?, 1)          evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d + 1, c + 11, c, d) [ a - d - 1 >= 0 /\ d - 1 >= 0 /\ c + d - 92 >= 0 /\ b + d - 102 >= 0 /\ a + d - 3 >= 0 /\ -a + d + 1 >= 0 /\ b - c - 10 >= 0 /\ c - 91 >= 0 /\ b + c - 192 >= 0 /\ -b + c + 10 >= 0 /\ a + c - 93 >= 0 /\ b - 101 >= 0 /\ a + b - 103 >= 0 /\ a - 2 >= 0 /\ 100 >= c ]
		(?, 1)          evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 1, c, d) [ a - d - 1 >= 0 /\ d - 1 >= 0 /\ c + d - 92 >= 0 /\ b + d - 102 >= 0 /\ a + d - 3 >= 0 /\ -a + d + 1 >= 0 /\ b - c - 10 >= 0 /\ c - 91 >= 0 /\ b + c - 192 >= 0 /\ -b + c + 10 >= 0 /\ a + c - 93 >= 0 /\ b - 101 >= 0 /\ a + b - 103 >= 0 /\ a - 2 >= 0 /\ c >= 101 ]
	start location:	evalsipma91start
	leaf cost:	4

A polynomial rank function with
	Pol(evalsipma91start) = -15*V_1 + 1488
	Pol(evalsipma91entryin) = -15*V_1 + 1488
	Pol(evalsipma91bb3in) = 165*V_1 - 15*V_2 + 1323
	Pol(evalsipma91bb2in) = 165*V_1 - 15*V_2 + 1323
	Pol(evalsipma91bb11in) = 165*V_1 - 15*V_2 + 1323
	Pol(evalsipma91bb5in) = 165*V_1 - 15*V_2 + 1322
	Pol(evalsipma91bb8in) = -15*V_3 + 165*V_4 + 1336
orients all transitions weakly and the transitions
	evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d + 1, c + 11, c, d) [ a - d - 1 >= 0 /\ d - 1 >= 0 /\ c + d - 92 >= 0 /\ b + d - 102 >= 0 /\ a + d - 3 >= 0 /\ -a + d + 1 >= 0 /\ b - c - 10 >= 0 /\ c - 91 >= 0 /\ b + c - 192 >= 0 /\ -b + c + 10 >= 0 /\ a + c - 93 >= 0 /\ b - 101 >= 0 /\ a + b - 103 >= 0 /\ a - 2 >= 0 /\ 100 >= c ]
	evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ b - 101 >= 0 /\ a + b - 103 >= 0 /\ a - 2 >= 0 /\ 110 >= b ]
strictly and produces the following problem:
10:	T:
		(1, 1)              evalsipma91start(a, b, c, d) -> evalsipma91entryin(a, b, c, d)
		(1, 1)              evalsipma91entryin(a, b, c, d) -> evalsipma91bb3in(1, a, c, d) [ 100 >= a ]
		(a + 103, 1)        evalsipma91bb3in(a, b, c, d) -> evalsipma91bb2in(a, b, c, d) [ a - 1 >= 0 /\ 100 >= b ]
		(a + 103, 1)        evalsipma91bb2in(a, b, c, d) -> evalsipma91bb3in(a + 1, b + 11, c, d) [ -b + 100 >= 0 /\ a - b + 99 >= 0 /\ a - 1 >= 0 ]
		(1, 1)              evalsipma91bb3in(a, b, c, d) -> evalsipma91bb11in(a, b, c, d) [ a - 1 >= 0 /\ b >= 101 ]
		(?, 1)              evalsipma91bb11in(a, b, c, d) -> evalsipma91bb5in(a, b, c, d) [ b - 101 >= 0 /\ a + b - 102 >= 0 /\ a - 1 >= 0 /\ a >= 2 ]
		(15*a + 1488, 1)    evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ b - 101 >= 0 /\ a + b - 103 >= 0 /\ a - 2 >= 0 /\ 110 >= b ]
		(?, 1)              evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ b - 101 >= 0 /\ a + b - 103 >= 0 /\ a - 2 >= 0 /\ a >= 3 ]
		(15*a + 1488, 1)    evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d + 1, c + 11, c, d) [ a - d - 1 >= 0 /\ d - 1 >= 0 /\ c + d - 92 >= 0 /\ b + d - 102 >= 0 /\ a + d - 3 >= 0 /\ -a + d + 1 >= 0 /\ b - c - 10 >= 0 /\ c - 91 >= 0 /\ b + c - 192 >= 0 /\ -b + c + 10 >= 0 /\ a + c - 93 >= 0 /\ b - 101 >= 0 /\ a + b - 103 >= 0 /\ a - 2 >= 0 /\ 100 >= c ]
		(?, 1)              evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 1, c, d) [ a - d - 1 >= 0 /\ d - 1 >= 0 /\ c + d - 92 >= 0 /\ b + d - 102 >= 0 /\ a + d - 3 >= 0 /\ -a + d + 1 >= 0 /\ b - c - 10 >= 0 /\ c - 91 >= 0 /\ b + c - 192 >= 0 /\ -b + c + 10 >= 0 /\ a + c - 93 >= 0 /\ b - 101 >= 0 /\ a + b - 103 >= 0 /\ a - 2 >= 0 /\ c >= 101 ]
	start location:	evalsipma91start
	leaf cost:	4

A polynomial rank function with
	Pol(evalsipma91bb8in) = 3*V_4 - 2
	Pol(evalsipma91bb11in) = 3*V_1 - 3
	Pol(evalsipma91bb5in) = 3*V_1 - 4
and size complexities
	S("evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 1, c, d) [ a - d - 1 >= 0 /\\ d - 1 >= 0 /\\ c + d - 92 >= 0 /\\ b + d - 102 >= 0 /\\ a + d - 3 >= 0 /\\ -a + d + 1 >= 0 /\\ b - c - 10 >= 0 /\\ c - 91 >= 0 /\\ b + c - 192 >= 0 /\\ -b + c + 10 >= 0 /\\ a + c - 93 >= 0 /\\ b - 101 >= 0 /\\ a + b - 103 >= 0 /\\ a - 2 >= 0 /\\ c >= 101 ]", 0-0) = a + 104
	S("evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 1, c, d) [ a - d - 1 >= 0 /\\ d - 1 >= 0 /\\ c + d - 92 >= 0 /\\ b + d - 102 >= 0 /\\ a + d - 3 >= 0 /\\ -a + d + 1 >= 0 /\\ b - c - 10 >= 0 /\\ c - 91 >= 0 /\\ b + c - 192 >= 0 /\\ -b + c + 10 >= 0 /\\ a + c - 93 >= 0 /\\ b - 101 >= 0 /\\ a + b - 103 >= 0 /\\ a - 2 >= 0 /\\ c >= 101 ]", 0-1) = a + 222
	S("evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 1, c, d) [ a - d - 1 >= 0 /\\ d - 1 >= 0 /\\ c + d - 92 >= 0 /\\ b + d - 102 >= 0 /\\ a + d - 3 >= 0 /\\ -a + d + 1 >= 0 /\\ b - c - 10 >= 0 /\\ c - 91 >= 0 /\\ b + c - 192 >= 0 /\\ -b + c + 10 >= 0 /\\ a + c - 93 >= 0 /\\ b - 101 >= 0 /\\ a + b - 103 >= 0 /\\ a - 2 >= 0 /\\ c >= 101 ]", 0-2) = a + 222
	S("evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 1, c, d) [ a - d - 1 >= 0 /\\ d - 1 >= 0 /\\ c + d - 92 >= 0 /\\ b + d - 102 >= 0 /\\ a + d - 3 >= 0 /\\ -a + d + 1 >= 0 /\\ b - c - 10 >= 0 /\\ c - 91 >= 0 /\\ b + c - 192 >= 0 /\\ -b + c + 10 >= 0 /\\ a + c - 93 >= 0 /\\ b - 101 >= 0 /\\ a + b - 103 >= 0 /\\ a - 2 >= 0 /\\ c >= 101 ]", 0-3) = a + 104
	S("evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d + 1, c + 11, c, d) [ a - d - 1 >= 0 /\\ d - 1 >= 0 /\\ c + d - 92 >= 0 /\\ b + d - 102 >= 0 /\\ a + d - 3 >= 0 /\\ -a + d + 1 >= 0 /\\ b - c - 10 >= 0 /\\ c - 91 >= 0 /\\ b + c - 192 >= 0 /\\ -b + c + 10 >= 0 /\\ a + c - 93 >= 0 /\\ b - 101 >= 0 /\\ a + b - 103 >= 0 /\\ a - 2 >= 0 /\\ 100 >= c ]", 0-0) = a + 104
	S("evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d + 1, c + 11, c, d) [ a - d - 1 >= 0 /\\ d - 1 >= 0 /\\ c + d - 92 >= 0 /\\ b + d - 102 >= 0 /\\ a + d - 3 >= 0 /\\ -a + d + 1 >= 0 /\\ b - c - 10 >= 0 /\\ c - 91 >= 0 /\\ b + c - 192 >= 0 /\\ -b + c + 10 >= 0 /\\ a + c - 93 >= 0 /\\ b - 101 >= 0 /\\ a + b - 103 >= 0 /\\ a - 2 >= 0 /\\ 100 >= c ]", 0-1) = 111
	S("evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d + 1, c + 11, c, d) [ a - d - 1 >= 0 /\\ d - 1 >= 0 /\\ c + d - 92 >= 0 /\\ b + d - 102 >= 0 /\\ a + d - 3 >= 0 /\\ -a + d + 1 >= 0 /\\ b - c - 10 >= 0 /\\ c - 91 >= 0 /\\ b + c - 192 >= 0 /\\ -b + c + 10 >= 0 /\\ a + c - 93 >= 0 /\\ b - 101 >= 0 /\\ a + b - 103 >= 0 /\\ a - 2 >= 0 /\\ 100 >= c ]", 0-2) = 100
	S("evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d + 1, c + 11, c, d) [ a - d - 1 >= 0 /\\ d - 1 >= 0 /\\ c + d - 92 >= 0 /\\ b + d - 102 >= 0 /\\ a + d - 3 >= 0 /\\ -a + d + 1 >= 0 /\\ b - c - 10 >= 0 /\\ c - 91 >= 0 /\\ b + c - 192 >= 0 /\\ -b + c + 10 >= 0 /\\ a + c - 93 >= 0 /\\ b - 101 >= 0 /\\ a + b - 103 >= 0 /\\ a - 2 >= 0 /\\ 100 >= c ]", 0-3) = a + 104
	S("evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ b - 101 >= 0 /\\ a + b - 103 >= 0 /\\ a - 2 >= 0 /\\ a >= 3 ]", 0-0) = a + 104
	S("evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ b - 101 >= 0 /\\ a + b - 103 >= 0 /\\ a - 2 >= 0 /\\ a >= 3 ]", 0-1) = a + 222
	S("evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ b - 101 >= 0 /\\ a + b - 103 >= 0 /\\ a - 2 >= 0 /\\ a >= 3 ]", 0-2) = a + 222
	S("evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ b - 101 >= 0 /\\ a + b - 103 >= 0 /\\ a - 2 >= 0 /\\ a >= 3 ]", 0-3) = a + 104
	S("evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ b - 101 >= 0 /\\ a + b - 103 >= 0 /\\ a - 2 >= 0 /\\ 110 >= b ]", 0-0) = a + 104
	S("evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ b - 101 >= 0 /\\ a + b - 103 >= 0 /\\ a - 2 >= 0 /\\ 110 >= b ]", 0-1) = 110
	S("evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ b - 101 >= 0 /\\ a + b - 103 >= 0 /\\ a - 2 >= 0 /\\ 110 >= b ]", 0-2) = 100
	S("evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ b - 101 >= 0 /\\ a + b - 103 >= 0 /\\ a - 2 >= 0 /\\ 110 >= b ]", 0-3) = a + 104
	S("evalsipma91bb11in(a, b, c, d) -> evalsipma91bb5in(a, b, c, d) [ b - 101 >= 0 /\\ a + b - 102 >= 0 /\\ a - 1 >= 0 /\\ a >= 2 ]", 0-0) = a + 104
	S("evalsipma91bb11in(a, b, c, d) -> evalsipma91bb5in(a, b, c, d) [ b - 101 >= 0 /\\ a + b - 102 >= 0 /\\ a - 1 >= 0 /\\ a >= 2 ]", 0-1) = a + 222
	S("evalsipma91bb11in(a, b, c, d) -> evalsipma91bb5in(a, b, c, d) [ b - 101 >= 0 /\\ a + b - 102 >= 0 /\\ a - 1 >= 0 /\\ a >= 2 ]", 0-2) = a + c + 322
	S("evalsipma91bb11in(a, b, c, d) -> evalsipma91bb5in(a, b, c, d) [ b - 101 >= 0 /\\ a + b - 102 >= 0 /\\ a - 1 >= 0 /\\ a >= 2 ]", 0-3) = a + d + 104
	S("evalsipma91bb3in(a, b, c, d) -> evalsipma91bb11in(a, b, c, d) [ a - 1 >= 0 /\\ b >= 101 ]", 0-0) = a + 104
	S("evalsipma91bb3in(a, b, c, d) -> evalsipma91bb11in(a, b, c, d) [ a - 1 >= 0 /\\ b >= 101 ]", 0-1) = a + 111
	S("evalsipma91bb3in(a, b, c, d) -> evalsipma91bb11in(a, b, c, d) [ a - 1 >= 0 /\\ b >= 101 ]", 0-2) = c
	S("evalsipma91bb3in(a, b, c, d) -> evalsipma91bb11in(a, b, c, d) [ a - 1 >= 0 /\\ b >= 101 ]", 0-3) = d
	S("evalsipma91bb2in(a, b, c, d) -> evalsipma91bb3in(a + 1, b + 11, c, d) [ -b + 100 >= 0 /\\ a - b + 99 >= 0 /\\ a - 1 >= 0 ]", 0-0) = a + 104
	S("evalsipma91bb2in(a, b, c, d) -> evalsipma91bb3in(a + 1, b + 11, c, d) [ -b + 100 >= 0 /\\ a - b + 99 >= 0 /\\ a - 1 >= 0 ]", 0-1) = a + 111
	S("evalsipma91bb2in(a, b, c, d) -> evalsipma91bb3in(a + 1, b + 11, c, d) [ -b + 100 >= 0 /\\ a - b + 99 >= 0 /\\ a - 1 >= 0 ]", 0-2) = c
	S("evalsipma91bb2in(a, b, c, d) -> evalsipma91bb3in(a + 1, b + 11, c, d) [ -b + 100 >= 0 /\\ a - b + 99 >= 0 /\\ a - 1 >= 0 ]", 0-3) = d
	S("evalsipma91bb3in(a, b, c, d) -> evalsipma91bb2in(a, b, c, d) [ a - 1 >= 0 /\\ 100 >= b ]", 0-0) = a + 104
	S("evalsipma91bb3in(a, b, c, d) -> evalsipma91bb2in(a, b, c, d) [ a - 1 >= 0 /\\ 100 >= b ]", 0-1) = a + 111
	S("evalsipma91bb3in(a, b, c, d) -> evalsipma91bb2in(a, b, c, d) [ a - 1 >= 0 /\\ 100 >= b ]", 0-2) = c
	S("evalsipma91bb3in(a, b, c, d) -> evalsipma91bb2in(a, b, c, d) [ a - 1 >= 0 /\\ 100 >= b ]", 0-3) = d
	S("evalsipma91entryin(a, b, c, d) -> evalsipma91bb3in(1, a, c, d) [ 100 >= a ]", 0-0) = 1
	S("evalsipma91entryin(a, b, c, d) -> evalsipma91bb3in(1, a, c, d) [ 100 >= a ]", 0-1) = a
	S("evalsipma91entryin(a, b, c, d) -> evalsipma91bb3in(1, a, c, d) [ 100 >= a ]", 0-2) = c
	S("evalsipma91entryin(a, b, c, d) -> evalsipma91bb3in(1, a, c, d) [ 100 >= a ]", 0-3) = d
	S("evalsipma91start(a, b, c, d) -> evalsipma91entryin(a, b, c, d)", 0-0) = a
	S("evalsipma91start(a, b, c, d) -> evalsipma91entryin(a, b, c, d)", 0-1) = b
	S("evalsipma91start(a, b, c, d) -> evalsipma91entryin(a, b, c, d)", 0-2) = c
	S("evalsipma91start(a, b, c, d) -> evalsipma91entryin(a, b, c, d)", 0-3) = d
orients the transitions
	evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 1, c, d) [ a - d - 1 >= 0 /\ d - 1 >= 0 /\ c + d - 92 >= 0 /\ b + d - 102 >= 0 /\ a + d - 3 >= 0 /\ -a + d + 1 >= 0 /\ b - c - 10 >= 0 /\ c - 91 >= 0 /\ b + c - 192 >= 0 /\ -b + c + 10 >= 0 /\ a + c - 93 >= 0 /\ b - 101 >= 0 /\ a + b - 103 >= 0 /\ a - 2 >= 0 /\ c >= 101 ]
	evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ b - 101 >= 0 /\ a + b - 103 >= 0 /\ a - 2 >= 0 /\ a >= 3 ]
	evalsipma91bb11in(a, b, c, d) -> evalsipma91bb5in(a, b, c, d) [ b - 101 >= 0 /\ a + b - 102 >= 0 /\ a - 1 >= 0 /\ a >= 2 ]
weakly and the transitions
	evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 1, c, d) [ a - d - 1 >= 0 /\ d - 1 >= 0 /\ c + d - 92 >= 0 /\ b + d - 102 >= 0 /\ a + d - 3 >= 0 /\ -a + d + 1 >= 0 /\ b - c - 10 >= 0 /\ c - 91 >= 0 /\ b + c - 192 >= 0 /\ -b + c + 10 >= 0 /\ a + c - 93 >= 0 /\ b - 101 >= 0 /\ a + b - 103 >= 0 /\ a - 2 >= 0 /\ c >= 101 ]
	evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ b - 101 >= 0 /\ a + b - 103 >= 0 /\ a - 2 >= 0 /\ a >= 3 ]
	evalsipma91bb11in(a, b, c, d) -> evalsipma91bb5in(a, b, c, d) [ b - 101 >= 0 /\ a + b - 102 >= 0 /\ a - 1 >= 0 /\ a >= 2 ]
strictly and produces the following problem:
11:	T:
		(1, 1)                           evalsipma91start(a, b, c, d) -> evalsipma91entryin(a, b, c, d)
		(1, 1)                           evalsipma91entryin(a, b, c, d) -> evalsipma91bb3in(1, a, c, d) [ 100 >= a ]
		(a + 103, 1)                     evalsipma91bb3in(a, b, c, d) -> evalsipma91bb2in(a, b, c, d) [ a - 1 >= 0 /\ 100 >= b ]
		(a + 103, 1)                     evalsipma91bb2in(a, b, c, d) -> evalsipma91bb3in(a + 1, b + 11, c, d) [ -b + 100 >= 0 /\ a - b + 99 >= 0 /\ a - 1 >= 0 ]
		(1, 1)                           evalsipma91bb3in(a, b, c, d) -> evalsipma91bb11in(a, b, c, d) [ a - 1 >= 0 /\ b >= 101 ]
		(45*a^2 + 9192*a + 469035, 1)    evalsipma91bb11in(a, b, c, d) -> evalsipma91bb5in(a, b, c, d) [ b - 101 >= 0 /\ a + b - 102 >= 0 /\ a - 1 >= 0 /\ a >= 2 ]
		(15*a + 1488, 1)                 evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ b - 101 >= 0 /\ a + b - 103 >= 0 /\ a - 2 >= 0 /\ 110 >= b ]
		(45*a^2 + 9192*a + 469035, 1)    evalsipma91bb5in(a, b, c, d) -> evalsipma91bb8in(a, b, b - 10, a - 1) [ b - 101 >= 0 /\ a + b - 103 >= 0 /\ a - 2 >= 0 /\ a >= 3 ]
		(15*a + 1488, 1)                 evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d + 1, c + 11, c, d) [ a - d - 1 >= 0 /\ d - 1 >= 0 /\ c + d - 92 >= 0 /\ b + d - 102 >= 0 /\ a + d - 3 >= 0 /\ -a + d + 1 >= 0 /\ b - c - 10 >= 0 /\ c - 91 >= 0 /\ b + c - 192 >= 0 /\ -b + c + 10 >= 0 /\ a + c - 93 >= 0 /\ b - 101 >= 0 /\ a + b - 103 >= 0 /\ a - 2 >= 0 /\ 100 >= c ]
		(45*a^2 + 9192*a + 469035, 1)    evalsipma91bb8in(a, b, c, d) -> evalsipma91bb11in(d, c + 1, c, d) [ a - d - 1 >= 0 /\ d - 1 >= 0 /\ c + d - 92 >= 0 /\ b + d - 102 >= 0 /\ a + d - 3 >= 0 /\ -a + d + 1 >= 0 /\ b - c - 10 >= 0 /\ c - 91 >= 0 /\ b + c - 192 >= 0 /\ -b + c + 10 >= 0 /\ a + c - 93 >= 0 /\ b - 101 >= 0 /\ a + b - 103 >= 0 /\ a - 2 >= 0 /\ c >= 101 ]
	start location:	evalsipma91start
	leaf cost:	4

Complexity upper bound 27608*a + 135*a^2 + 1410294

Time: 1.092 sec (SMT: 1.026 sec)