MAYBE

Initial complexity problem:
1:	T:
		(1, 1)    evalEx5start(a, b, c, d, e) -> evalEx5entryin(a, b, c, d, e)
		(?, 1)    evalEx5entryin(a, b, c, d, e) -> evalEx5bb6in(0, a, c, d, e)
		(?, 1)    evalEx5bb6in(a, b, c, d, e) -> evalEx5bb3in(a, b, 0, b, e) [ b >= a + 1 ]
		(?, 1)    evalEx5bb6in(a, b, c, d, e) -> evalEx5returnin(a, b, c, d, e) [ a >= b ]
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ 0 >= f + 1 ]
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ f >= 1 ]
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb4in(a, b, c, d, e)
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ 0 >= f + 1 ]
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ 0 >= f + 1 /\ f >= 1 ]
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ f >= 1 ]
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d - 1, e) [ 0 >= 1 ]
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d - 1, e) [ 0 >= 1 ]
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d) [ 0 >= 1 ]
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d) [ 0 >= 1 ]
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d, e)
		(?, 1)    evalEx5bb2in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, e, e)
		(?, 1)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a + 1, d, c, d, e) [ c = 0 ]
		(?, 1)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a, d, c, d, e) [ 0 >= c + 1 ]
		(?, 1)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a, d, c, d, e) [ c >= 1 ]
		(?, 1)    evalEx5returnin(a, b, c, d, e) -> evalEx5stop(a, b, c, d, e)
	start location:	evalEx5start
	leaf cost:	0

Testing for unsatisfiable constraints removes the following transitions from problem 1:
	evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ 0 >= f + 1 /\ f >= 1 ]
	evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d - 1, e) [ 0 >= 1 ]
	evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d - 1, e) [ 0 >= 1 ]
	evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d) [ 0 >= 1 ]
	evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d) [ 0 >= 1 ]
We thus obtain the following problem:
2:	T:
		(1, 1)    evalEx5start(a, b, c, d, e) -> evalEx5entryin(a, b, c, d, e)
		(?, 1)    evalEx5entryin(a, b, c, d, e) -> evalEx5bb6in(0, a, c, d, e)
		(?, 1)    evalEx5bb6in(a, b, c, d, e) -> evalEx5bb3in(a, b, 0, b, e) [ b >= a + 1 ]
		(?, 1)    evalEx5bb6in(a, b, c, d, e) -> evalEx5returnin(a, b, c, d, e) [ a >= b ]
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ 0 >= f + 1 ]
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ f >= 1 ]
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb4in(a, b, c, d, e)
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ 0 >= f + 1 ]
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ f >= 1 ]
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d, e)
		(?, 1)    evalEx5bb2in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, e, e)
		(?, 1)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a + 1, d, c, d, e) [ c = 0 ]
		(?, 1)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a, d, c, d, e) [ 0 >= c + 1 ]
		(?, 1)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a, d, c, d, e) [ c >= 1 ]
		(?, 1)    evalEx5returnin(a, b, c, d, e) -> evalEx5stop(a, b, c, d, e)
	start location:	evalEx5start
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalEx5start(a, b, c, d, e) -> evalEx5entryin(a, b, c, d, e)
		(?, 1)    evalEx5entryin(a, b, c, d, e) -> evalEx5bb6in(0, a, c, d, e)
		(?, 1)    evalEx5bb6in(a, b, c, d, e) -> evalEx5bb3in(a, b, 0, b, e) [ b >= a + 1 ]
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ 0 >= f + 1 ]
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ f >= 1 ]
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb4in(a, b, c, d, e)
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ 0 >= f + 1 ]
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ f >= 1 ]
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d, e)
		(?, 1)    evalEx5bb2in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, e, e)
		(?, 1)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a + 1, d, c, d, e) [ c = 0 ]
		(?, 1)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a, d, c, d, e) [ 0 >= c + 1 ]
		(?, 1)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a, d, c, d, e) [ c >= 1 ]
	start location:	evalEx5start
	leaf cost:	2

Repeatedly propagating knowledge in problem 3 produces the following problem:
4:	T:
		(1, 1)    evalEx5start(a, b, c, d, e) -> evalEx5entryin(a, b, c, d, e)
		(1, 1)    evalEx5entryin(a, b, c, d, e) -> evalEx5bb6in(0, a, c, d, e)
		(?, 1)    evalEx5bb6in(a, b, c, d, e) -> evalEx5bb3in(a, b, 0, b, e) [ b >= a + 1 ]
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ 0 >= f + 1 ]
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ f >= 1 ]
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb4in(a, b, c, d, e)
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ 0 >= f + 1 ]
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ f >= 1 ]
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d, e)
		(?, 1)    evalEx5bb2in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, e, e)
		(?, 1)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a + 1, d, c, d, e) [ c = 0 ]
		(?, 1)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a, d, c, d, e) [ 0 >= c + 1 ]
		(?, 1)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a, d, c, d, e) [ c >= 1 ]
	start location:	evalEx5start
	leaf cost:	2

By chaining the transition evalEx5start(a, b, c, d, e) -> evalEx5entryin(a, b, c, d, e) with all transitions in problem 4, the following new transition is obtained:
	evalEx5start(a, b, c, d, e) -> evalEx5bb6in(0, a, c, d, e)
We thus obtain the following problem:
5:	T:
		(1, 2)    evalEx5start(a, b, c, d, e) -> evalEx5bb6in(0, a, c, d, e)
		(1, 1)    evalEx5entryin(a, b, c, d, e) -> evalEx5bb6in(0, a, c, d, e)
		(?, 1)    evalEx5bb6in(a, b, c, d, e) -> evalEx5bb3in(a, b, 0, b, e) [ b >= a + 1 ]
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ 0 >= f + 1 ]
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ f >= 1 ]
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb4in(a, b, c, d, e)
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ 0 >= f + 1 ]
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ f >= 1 ]
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d, e)
		(?, 1)    evalEx5bb2in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, e, e)
		(?, 1)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a + 1, d, c, d, e) [ c = 0 ]
		(?, 1)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a, d, c, d, e) [ 0 >= c + 1 ]
		(?, 1)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a, d, c, d, e) [ c >= 1 ]
	start location:	evalEx5start
	leaf cost:	2

Testing for reachability in the complexity graph removes the following transition from problem 5:
	evalEx5entryin(a, b, c, d, e) -> evalEx5bb6in(0, a, c, d, e)
We thus obtain the following problem:
6:	T:
		(?, 1)    evalEx5bb2in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, e, e)
		(?, 1)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a, d, c, d, e) [ c >= 1 ]
		(?, 1)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a, d, c, d, e) [ 0 >= c + 1 ]
		(?, 1)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a + 1, d, c, d, e) [ c = 0 ]
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d, e)
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ f >= 1 ]
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ 0 >= f + 1 ]
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb4in(a, b, c, d, e)
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ f >= 1 ]
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ 0 >= f + 1 ]
		(?, 1)    evalEx5bb6in(a, b, c, d, e) -> evalEx5bb3in(a, b, 0, b, e) [ b >= a + 1 ]
		(1, 2)    evalEx5start(a, b, c, d, e) -> evalEx5bb6in(0, a, c, d, e)
	start location:	evalEx5start
	leaf cost:	2

By chaining the transition evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a, d, c, d, e) [ c >= 1 ] with all transitions in problem 6, the following new transition is obtained:
	evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ c >= 1 /\ d >= a + 1 ]
We thus obtain the following problem:
7:	T:
		(?, 2)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ c >= 1 /\ d >= a + 1 ]
		(?, 1)    evalEx5bb2in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, e, e)
		(?, 1)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a, d, c, d, e) [ 0 >= c + 1 ]
		(?, 1)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a + 1, d, c, d, e) [ c = 0 ]
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d, e)
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ f >= 1 ]
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ 0 >= f + 1 ]
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb4in(a, b, c, d, e)
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ f >= 1 ]
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ 0 >= f + 1 ]
		(?, 1)    evalEx5bb6in(a, b, c, d, e) -> evalEx5bb3in(a, b, 0, b, e) [ b >= a + 1 ]
		(1, 2)    evalEx5start(a, b, c, d, e) -> evalEx5bb6in(0, a, c, d, e)
	start location:	evalEx5start
	leaf cost:	2

By chaining the transition evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a, d, c, d, e) [ 0 >= c + 1 ] with all transitions in problem 7, the following new transition is obtained:
	evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ 0 >= c + 1 /\ d >= a + 1 ]
We thus obtain the following problem:
8:	T:
		(?, 2)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ 0 >= c + 1 /\ d >= a + 1 ]
		(?, 2)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ c >= 1 /\ d >= a + 1 ]
		(?, 1)    evalEx5bb2in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, e, e)
		(?, 1)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a + 1, d, c, d, e) [ c = 0 ]
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d, e)
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ f >= 1 ]
		(?, 1)    evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ 0 >= f + 1 ]
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb4in(a, b, c, d, e)
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ f >= 1 ]
		(?, 1)    evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ 0 >= f + 1 ]
		(?, 1)    evalEx5bb6in(a, b, c, d, e) -> evalEx5bb3in(a, b, 0, b, e) [ b >= a + 1 ]
		(1, 2)    evalEx5start(a, b, c, d, e) -> evalEx5bb6in(0, a, c, d, e)
	start location:	evalEx5start
	leaf cost:	2

A polynomial rank function with
	Pol(evalEx5bb4in) = -2*V_1 + 2*V_4 - 1
	Pol(evalEx5bb3in) = -2*V_1 + 2*V_4 - 1
	Pol(evalEx5bb2in) = -2*V_1 + 2*V_5
	Pol(evalEx5bb6in) = -2*V_1 + 2*V_2
	Pol(evalEx5bb1in) = -2*V_1 + 2*V_4 - 1
	Pol(evalEx5start) = 2*V_1
orients all transitions weakly and the transition
	evalEx5bb6in(a, b, c, d, e) -> evalEx5bb3in(a, b, 0, b, e) [ b >= a + 1 ]
strictly and produces the following problem:
9:	T:
		(?, 2)      evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ 0 >= c + 1 /\ d >= a + 1 ]
		(?, 2)      evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ c >= 1 /\ d >= a + 1 ]
		(?, 1)      evalEx5bb2in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, e, e)
		(?, 1)      evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a + 1, d, c, d, e) [ c = 0 ]
		(?, 1)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d, e)
		(?, 1)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ f >= 1 ]
		(?, 1)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ 0 >= f + 1 ]
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb4in(a, b, c, d, e)
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ f >= 1 ]
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ 0 >= f + 1 ]
		(2*a, 1)    evalEx5bb6in(a, b, c, d, e) -> evalEx5bb3in(a, b, 0, b, e) [ b >= a + 1 ]
		(1, 2)      evalEx5start(a, b, c, d, e) -> evalEx5bb6in(0, a, c, d, e)
	start location:	evalEx5start
	leaf cost:	2

A polynomial rank function with
	Pol(evalEx5bb4in) = 1
	Pol(evalEx5bb6in) = 0
	Pol(evalEx5bb3in) = 1
	Pol(evalEx5bb1in) = 1
	Pol(evalEx5bb2in) = 1
and size complexities
	S("evalEx5start(a, b, c, d, e) -> evalEx5bb6in(0, a, c, d, e)", 0-0) = 0
	S("evalEx5start(a, b, c, d, e) -> evalEx5bb6in(0, a, c, d, e)", 0-1) = a
	S("evalEx5start(a, b, c, d, e) -> evalEx5bb6in(0, a, c, d, e)", 0-2) = c
	S("evalEx5start(a, b, c, d, e) -> evalEx5bb6in(0, a, c, d, e)", 0-3) = d
	S("evalEx5start(a, b, c, d, e) -> evalEx5bb6in(0, a, c, d, e)", 0-4) = e
	S("evalEx5bb6in(a, b, c, d, e) -> evalEx5bb3in(a, b, 0, b, e) [ b >= a + 1 ]", 0-0) = ?
	S("evalEx5bb6in(a, b, c, d, e) -> evalEx5bb3in(a, b, 0, b, e) [ b >= a + 1 ]", 0-1) = ?
	S("evalEx5bb6in(a, b, c, d, e) -> evalEx5bb3in(a, b, 0, b, e) [ b >= a + 1 ]", 0-2) = 0
	S("evalEx5bb6in(a, b, c, d, e) -> evalEx5bb3in(a, b, 0, b, e) [ b >= a + 1 ]", 0-3) = ?
	S("evalEx5bb6in(a, b, c, d, e) -> evalEx5bb3in(a, b, 0, b, e) [ b >= a + 1 ]", 0-4) = ?
	S("evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ 0 >= f + 1 ]", 0-0) = ?
	S("evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ 0 >= f + 1 ]", 0-1) = ?
	S("evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ 0 >= f + 1 ]", 0-2) = 1
	S("evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ 0 >= f + 1 ]", 0-3) = ?
	S("evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ 0 >= f + 1 ]", 0-4) = ?
	S("evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ f >= 1 ]", 0-0) = ?
	S("evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ f >= 1 ]", 0-1) = ?
	S("evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ f >= 1 ]", 0-2) = 1
	S("evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ f >= 1 ]", 0-3) = ?
	S("evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ f >= 1 ]", 0-4) = ?
	S("evalEx5bb3in(a, b, c, d, e) -> evalEx5bb4in(a, b, c, d, e)", 0-0) = ?
	S("evalEx5bb3in(a, b, c, d, e) -> evalEx5bb4in(a, b, c, d, e)", 0-1) = ?
	S("evalEx5bb3in(a, b, c, d, e) -> evalEx5bb4in(a, b, c, d, e)", 0-2) = 1
	S("evalEx5bb3in(a, b, c, d, e) -> evalEx5bb4in(a, b, c, d, e)", 0-3) = ?
	S("evalEx5bb3in(a, b, c, d, e) -> evalEx5bb4in(a, b, c, d, e)", 0-4) = ?
	S("evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ 0 >= f + 1 ]", 0-0) = ?
	S("evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ 0 >= f + 1 ]", 0-1) = ?
	S("evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ 0 >= f + 1 ]", 0-2) = 1
	S("evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ 0 >= f + 1 ]", 0-3) = ?
	S("evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ 0 >= f + 1 ]", 0-4) = ?
	S("evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ f >= 1 ]", 0-0) = ?
	S("evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ f >= 1 ]", 0-1) = ?
	S("evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ f >= 1 ]", 0-2) = 1
	S("evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ f >= 1 ]", 0-3) = ?
	S("evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ f >= 1 ]", 0-4) = ?
	S("evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d, e)", 0-0) = ?
	S("evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d, e)", 0-1) = ?
	S("evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d, e)", 0-2) = 1
	S("evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d, e)", 0-3) = ?
	S("evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d, e)", 0-4) = ?
	S("evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a + 1, d, c, d, e) [ c = 0 ]", 0-0) = ?
	S("evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a + 1, d, c, d, e) [ c = 0 ]", 0-1) = ?
	S("evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a + 1, d, c, d, e) [ c = 0 ]", 0-2) = 0
	S("evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a + 1, d, c, d, e) [ c = 0 ]", 0-3) = ?
	S("evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a + 1, d, c, d, e) [ c = 0 ]", 0-4) = ?
	S("evalEx5bb2in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, e, e)", 0-0) = ?
	S("evalEx5bb2in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, e, e)", 0-1) = ?
	S("evalEx5bb2in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, e, e)", 0-2) = 1
	S("evalEx5bb2in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, e, e)", 0-3) = ?
	S("evalEx5bb2in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, e, e)", 0-4) = ?
	S("evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ c >= 1 /\\ d >= a + 1 ]", 0-0) = ?
	S("evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ c >= 1 /\\ d >= a + 1 ]", 0-1) = ?
	S("evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ c >= 1 /\\ d >= a + 1 ]", 0-2) = 0
	S("evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ c >= 1 /\\ d >= a + 1 ]", 0-3) = ?
	S("evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ c >= 1 /\\ d >= a + 1 ]", 0-4) = ?
	S("evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-0) = ?
	S("evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-1) = ?
	S("evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-2) = 0
	S("evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-3) = ?
	S("evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-4) = ?
orients the transitions
	evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a + 1, d, c, d, e) [ c = 0 ]
	evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ c >= 1 /\ d >= a + 1 ]
	evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ 0 >= c + 1 /\ d >= a + 1 ]
	evalEx5bb3in(a, b, c, d, e) -> evalEx5bb4in(a, b, c, d, e)
	evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ f >= 1 ]
	evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ 0 >= f + 1 ]
	evalEx5bb2in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, e, e)
	evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d, e)
	evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ f >= 1 ]
	evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ 0 >= f + 1 ]
weakly and the transition
	evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a + 1, d, c, d, e) [ c = 0 ]
strictly and produces the following problem:
10:	T:
		(?, 2)      evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ 0 >= c + 1 /\ d >= a + 1 ]
		(?, 2)      evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ c >= 1 /\ d >= a + 1 ]
		(?, 1)      evalEx5bb2in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, e, e)
		(2*a, 1)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a + 1, d, c, d, e) [ c = 0 ]
		(?, 1)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d, e)
		(?, 1)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ f >= 1 ]
		(?, 1)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ 0 >= f + 1 ]
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb4in(a, b, c, d, e)
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ f >= 1 ]
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ 0 >= f + 1 ]
		(2*a, 1)    evalEx5bb6in(a, b, c, d, e) -> evalEx5bb3in(a, b, 0, b, e) [ b >= a + 1 ]
		(1, 2)      evalEx5start(a, b, c, d, e) -> evalEx5bb6in(0, a, c, d, e)
	start location:	evalEx5start
	leaf cost:	2

By chaining the transition evalEx5bb4in(a, b, c, d, e) -> evalEx5bb6in(a + 1, d, c, d, e) [ c = 0 ] with all transitions in problem 10, the following new transition is obtained:
	evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a + 1, d, 0, d, e) [ c = 0 /\ d >= a + 2 ]
We thus obtain the following problem:
11:	T:
		(2*a, 2)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a + 1, d, 0, d, e) [ c = 0 /\ d >= a + 2 ]
		(?, 2)      evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ 0 >= c + 1 /\ d >= a + 1 ]
		(?, 2)      evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ c >= 1 /\ d >= a + 1 ]
		(?, 1)      evalEx5bb2in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, e, e)
		(?, 1)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d, e)
		(?, 1)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ f >= 1 ]
		(?, 1)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ 0 >= f + 1 ]
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb4in(a, b, c, d, e)
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ f >= 1 ]
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ 0 >= f + 1 ]
		(2*a, 1)    evalEx5bb6in(a, b, c, d, e) -> evalEx5bb3in(a, b, 0, b, e) [ b >= a + 1 ]
		(1, 2)      evalEx5start(a, b, c, d, e) -> evalEx5bb6in(0, a, c, d, e)
	start location:	evalEx5start
	leaf cost:	2

By chaining the transition evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ f >= 1 ] with all transitions in problem 11, the following new transition is obtained:
	evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, d - 1, d - 1) [ f >= 1 ]
We thus obtain the following problem:
12:	T:
		(?, 2)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, d - 1, d - 1) [ f >= 1 ]
		(2*a, 2)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a + 1, d, 0, d, e) [ c = 0 /\ d >= a + 2 ]
		(?, 2)      evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ 0 >= c + 1 /\ d >= a + 1 ]
		(?, 2)      evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ c >= 1 /\ d >= a + 1 ]
		(?, 1)      evalEx5bb2in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, e, e)
		(?, 1)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d, e)
		(?, 1)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ 0 >= f + 1 ]
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb4in(a, b, c, d, e)
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ f >= 1 ]
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ 0 >= f + 1 ]
		(2*a, 1)    evalEx5bb6in(a, b, c, d, e) -> evalEx5bb3in(a, b, 0, b, e) [ b >= a + 1 ]
		(1, 2)      evalEx5start(a, b, c, d, e) -> evalEx5bb6in(0, a, c, d, e)
	start location:	evalEx5start
	leaf cost:	2

By chaining the transition evalEx5bb1in(a, b, c, d, e) -> evalEx5bb2in(a, b, c, d, d - 1) [ 0 >= f + 1 ] with all transitions in problem 12, the following new transition is obtained:
	evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, d - 1, d - 1) [ 0 >= f + 1 ]
We thus obtain the following problem:
13:	T:
		(?, 2)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, d - 1, d - 1) [ 0 >= f + 1 ]
		(?, 2)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, d - 1, d - 1) [ f >= 1 ]
		(2*a, 2)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a + 1, d, 0, d, e) [ c = 0 /\ d >= a + 2 ]
		(?, 2)      evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ 0 >= c + 1 /\ d >= a + 1 ]
		(?, 2)      evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ c >= 1 /\ d >= a + 1 ]
		(?, 1)      evalEx5bb2in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, e, e)
		(?, 1)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d, e)
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb4in(a, b, c, d, e)
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ f >= 1 ]
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ 0 >= f + 1 ]
		(2*a, 1)    evalEx5bb6in(a, b, c, d, e) -> evalEx5bb3in(a, b, 0, b, e) [ b >= a + 1 ]
		(1, 2)      evalEx5start(a, b, c, d, e) -> evalEx5bb6in(0, a, c, d, e)
	start location:	evalEx5start
	leaf cost:	2

Testing for reachability in the complexity graph removes the following transition from problem 13:
	evalEx5bb2in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, e, e)
We thus obtain the following problem:
14:	T:
		(2*a, 2)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a + 1, d, 0, d, e) [ c = 0 /\ d >= a + 2 ]
		(?, 2)      evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ 0 >= c + 1 /\ d >= a + 1 ]
		(?, 2)      evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ c >= 1 /\ d >= a + 1 ]
		(?, 2)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, d - 1, d - 1) [ 0 >= f + 1 ]
		(?, 2)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, d - 1, d - 1) [ f >= 1 ]
		(?, 1)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d, e)
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb4in(a, b, c, d, e)
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ f >= 1 ]
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ 0 >= f + 1 ]
		(2*a, 1)    evalEx5bb6in(a, b, c, d, e) -> evalEx5bb3in(a, b, 0, b, e) [ b >= a + 1 ]
		(1, 2)      evalEx5start(a, b, c, d, e) -> evalEx5bb6in(0, a, c, d, e)
	start location:	evalEx5start
	leaf cost:	2

By chaining the transition evalEx5start(a, b, c, d, e) -> evalEx5bb6in(0, a, c, d, e) with all transitions in problem 14, the following new transition is obtained:
	evalEx5start(a, b, c, d, e) -> evalEx5bb3in(0, a, 0, a, e) [ a >= 1 ]
We thus obtain the following problem:
15:	T:
		(1, 3)      evalEx5start(a, b, c, d, e) -> evalEx5bb3in(0, a, 0, a, e) [ a >= 1 ]
		(2*a, 2)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a + 1, d, 0, d, e) [ c = 0 /\ d >= a + 2 ]
		(?, 2)      evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ 0 >= c + 1 /\ d >= a + 1 ]
		(?, 2)      evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ c >= 1 /\ d >= a + 1 ]
		(?, 2)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, d - 1, d - 1) [ 0 >= f + 1 ]
		(?, 2)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, d - 1, d - 1) [ f >= 1 ]
		(?, 1)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d, e)
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb4in(a, b, c, d, e)
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ f >= 1 ]
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ 0 >= f + 1 ]
		(2*a, 1)    evalEx5bb6in(a, b, c, d, e) -> evalEx5bb3in(a, b, 0, b, e) [ b >= a + 1 ]
	start location:	evalEx5start
	leaf cost:	2

Testing for reachability in the complexity graph removes the following transition from problem 15:
	evalEx5bb6in(a, b, c, d, e) -> evalEx5bb3in(a, b, 0, b, e) [ b >= a + 1 ]
We thus obtain the following problem:
16:	T:
		(2*a, 2)    evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a + 1, d, 0, d, e) [ c = 0 /\ d >= a + 2 ]
		(?, 2)      evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ 0 >= c + 1 /\ d >= a + 1 ]
		(?, 2)      evalEx5bb4in(a, b, c, d, e) -> evalEx5bb3in(a, d, 0, d, e) [ c >= 1 /\ d >= a + 1 ]
		(?, 2)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, d - 1, d - 1) [ 0 >= f + 1 ]
		(?, 2)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, 1, d - 1, d - 1) [ f >= 1 ]
		(?, 1)      evalEx5bb1in(a, b, c, d, e) -> evalEx5bb3in(a, b, c, d, e)
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb4in(a, b, c, d, e)
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ f >= 1 ]
		(?, 1)      evalEx5bb3in(a, b, c, d, e) -> evalEx5bb1in(a, b, c, d, e) [ 0 >= f + 1 ]
		(1, 3)      evalEx5start(a, b, c, d, e) -> evalEx5bb3in(0, a, 0, a, e) [ a >= 1 ]
	start location:	evalEx5start
	leaf cost:	2

Complexity upper bound ?

Time: 4.991 sec (SMT: 4.501 sec)