MAYBE

Initial complexity problem:
1:	T:
		(1, 1)    evalEx2start(a, b, c, d) -> evalEx2entryin(a, b, c, d)
		(?, 1)    evalEx2entryin(a, b, c, d) -> evalEx2bb3in(b, a, c, d)
		(?, 1)    evalEx2bb3in(a, b, c, d) -> evalEx2bbin(a, b, c, d) [ b >= 1 /\ a >= 1 ]
		(?, 1)    evalEx2bb3in(a, b, c, d) -> evalEx2returnin(a, b, c, d) [ 0 >= b ]
		(?, 1)    evalEx2bb3in(a, b, c, d) -> evalEx2returnin(a, b, c, d) [ 0 >= a ]
		(?, 1)    evalEx2bbin(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1)
		(?, 1)    evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ 0 >= e + 1 ]
		(?, 1)    evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ e >= 1 ]
		(?, 1)    evalEx2bb2in(a, b, c, d) -> evalEx2bb3in(c, d, c, d)
		(?, 1)    evalEx2bb1in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1)
		(?, 1)    evalEx2returnin(a, b, c, d) -> evalEx2stop(a, b, c, d)
	start location:	evalEx2start
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalEx2start(a, b, c, d) -> evalEx2entryin(a, b, c, d)
		(?, 1)    evalEx2entryin(a, b, c, d) -> evalEx2bb3in(b, a, c, d)
		(?, 1)    evalEx2bb3in(a, b, c, d) -> evalEx2bbin(a, b, c, d) [ b >= 1 /\ a >= 1 ]
		(?, 1)    evalEx2bbin(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1)
		(?, 1)    evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ 0 >= e + 1 ]
		(?, 1)    evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ e >= 1 ]
		(?, 1)    evalEx2bb2in(a, b, c, d) -> evalEx2bb3in(c, d, c, d)
		(?, 1)    evalEx2bb1in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1)
	start location:	evalEx2start
	leaf cost:	3

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalEx2start(a, b, c, d) -> evalEx2entryin(a, b, c, d)
		(1, 1)    evalEx2entryin(a, b, c, d) -> evalEx2bb3in(b, a, c, d)
		(?, 1)    evalEx2bb3in(a, b, c, d) -> evalEx2bbin(a, b, c, d) [ b >= 1 /\ a >= 1 ]
		(?, 1)    evalEx2bbin(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1)
		(?, 1)    evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ 0 >= e + 1 ]
		(?, 1)    evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ e >= 1 ]
		(?, 1)    evalEx2bb2in(a, b, c, d) -> evalEx2bb3in(c, d, c, d)
		(?, 1)    evalEx2bb1in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1)
	start location:	evalEx2start
	leaf cost:	3

A polynomial rank function with
	Pol(evalEx2start) = 3*V_1 + V_2 - 2
	Pol(evalEx2entryin) = 3*V_1 + V_2 - 2
	Pol(evalEx2bb3in) = V_1 + 3*V_2 - 2
	Pol(evalEx2bbin) = V_1 + 3*V_2 - 3
	Pol(evalEx2bb2in) = V_3 + 3*V_4 - 1
	Pol(evalEx2bb1in) = V_3 + 3*V_4 - 2
orients all transitions weakly and the transition
	evalEx2bb3in(a, b, c, d) -> evalEx2bbin(a, b, c, d) [ b >= 1 /\ a >= 1 ]
strictly and produces the following problem:
4:	T:
		(1, 1)              evalEx2start(a, b, c, d) -> evalEx2entryin(a, b, c, d)
		(1, 1)              evalEx2entryin(a, b, c, d) -> evalEx2bb3in(b, a, c, d)
		(3*a + b + 2, 1)    evalEx2bb3in(a, b, c, d) -> evalEx2bbin(a, b, c, d) [ b >= 1 /\ a >= 1 ]
		(?, 1)              evalEx2bbin(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1)
		(?, 1)              evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ 0 >= e + 1 ]
		(?, 1)              evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ e >= 1 ]
		(?, 1)              evalEx2bb2in(a, b, c, d) -> evalEx2bb3in(c, d, c, d)
		(?, 1)              evalEx2bb1in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1)
	start location:	evalEx2start
	leaf cost:	3

Repeatedly propagating knowledge in problem 4 produces the following problem:
5:	T:
		(1, 1)              evalEx2start(a, b, c, d) -> evalEx2entryin(a, b, c, d)
		(1, 1)              evalEx2entryin(a, b, c, d) -> evalEx2bb3in(b, a, c, d)
		(3*a + b + 2, 1)    evalEx2bb3in(a, b, c, d) -> evalEx2bbin(a, b, c, d) [ b >= 1 /\ a >= 1 ]
		(3*a + b + 2, 1)    evalEx2bbin(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1)
		(?, 1)              evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ 0 >= e + 1 ]
		(?, 1)              evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ e >= 1 ]
		(?, 1)              evalEx2bb2in(a, b, c, d) -> evalEx2bb3in(c, d, c, d)
		(?, 1)              evalEx2bb1in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1)
	start location:	evalEx2start
	leaf cost:	3

A polynomial rank function with
	Pol(evalEx2bb2in) = 1
	Pol(evalEx2bb3in) = 0
	Pol(evalEx2bb1in) = 1
and size complexities
	S("evalEx2bb1in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1)", 0-0) = ?
	S("evalEx2bb1in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1)", 0-1) = ?
	S("evalEx2bb1in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1)", 0-2) = ?
	S("evalEx2bb1in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1)", 0-3) = ?
	S("evalEx2bb2in(a, b, c, d) -> evalEx2bb3in(c, d, c, d)", 0-0) = ?
	S("evalEx2bb2in(a, b, c, d) -> evalEx2bb3in(c, d, c, d)", 0-1) = ?
	S("evalEx2bb2in(a, b, c, d) -> evalEx2bb3in(c, d, c, d)", 0-2) = ?
	S("evalEx2bb2in(a, b, c, d) -> evalEx2bb3in(c, d, c, d)", 0-3) = ?
	S("evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ e >= 1 ]", 0-0) = ?
	S("evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ e >= 1 ]", 0-1) = ?
	S("evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ e >= 1 ]", 0-2) = ?
	S("evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ e >= 1 ]", 0-3) = ?
	S("evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ 0 >= e + 1 ]", 0-0) = ?
	S("evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ 0 >= e + 1 ]", 0-1) = ?
	S("evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ 0 >= e + 1 ]", 0-2) = ?
	S("evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ 0 >= e + 1 ]", 0-3) = ?
	S("evalEx2bbin(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1)", 0-0) = ?
	S("evalEx2bbin(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1)", 0-1) = ?
	S("evalEx2bbin(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1)", 0-2) = ?
	S("evalEx2bbin(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1)", 0-3) = ?
	S("evalEx2bb3in(a, b, c, d) -> evalEx2bbin(a, b, c, d) [ b >= 1 /\\ a >= 1 ]", 0-0) = ?
	S("evalEx2bb3in(a, b, c, d) -> evalEx2bbin(a, b, c, d) [ b >= 1 /\\ a >= 1 ]", 0-1) = ?
	S("evalEx2bb3in(a, b, c, d) -> evalEx2bbin(a, b, c, d) [ b >= 1 /\\ a >= 1 ]", 0-2) = ?
	S("evalEx2bb3in(a, b, c, d) -> evalEx2bbin(a, b, c, d) [ b >= 1 /\\ a >= 1 ]", 0-3) = ?
	S("evalEx2entryin(a, b, c, d) -> evalEx2bb3in(b, a, c, d)", 0-0) = b
	S("evalEx2entryin(a, b, c, d) -> evalEx2bb3in(b, a, c, d)", 0-1) = a
	S("evalEx2entryin(a, b, c, d) -> evalEx2bb3in(b, a, c, d)", 0-2) = c
	S("evalEx2entryin(a, b, c, d) -> evalEx2bb3in(b, a, c, d)", 0-3) = d
	S("evalEx2start(a, b, c, d) -> evalEx2entryin(a, b, c, d)", 0-0) = a
	S("evalEx2start(a, b, c, d) -> evalEx2entryin(a, b, c, d)", 0-1) = b
	S("evalEx2start(a, b, c, d) -> evalEx2entryin(a, b, c, d)", 0-2) = c
	S("evalEx2start(a, b, c, d) -> evalEx2entryin(a, b, c, d)", 0-3) = d
orients the transitions
	evalEx2bb2in(a, b, c, d) -> evalEx2bb3in(c, d, c, d)
	evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ e >= 1 ]
	evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ 0 >= e + 1 ]
	evalEx2bb1in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1)
weakly and the transition
	evalEx2bb2in(a, b, c, d) -> evalEx2bb3in(c, d, c, d)
strictly and produces the following problem:
6:	T:
		(1, 1)              evalEx2start(a, b, c, d) -> evalEx2entryin(a, b, c, d)
		(1, 1)              evalEx2entryin(a, b, c, d) -> evalEx2bb3in(b, a, c, d)
		(3*a + b + 2, 1)    evalEx2bb3in(a, b, c, d) -> evalEx2bbin(a, b, c, d) [ b >= 1 /\ a >= 1 ]
		(3*a + b + 2, 1)    evalEx2bbin(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1)
		(?, 1)              evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ 0 >= e + 1 ]
		(?, 1)              evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ e >= 1 ]
		(3*a + b + 2, 1)    evalEx2bb2in(a, b, c, d) -> evalEx2bb3in(c, d, c, d)
		(?, 1)              evalEx2bb1in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1)
	start location:	evalEx2start
	leaf cost:	3

By chaining the transition evalEx2start(a, b, c, d) -> evalEx2entryin(a, b, c, d) with all transitions in problem 6, the following new transition is obtained:
	evalEx2start(a, b, c, d) -> evalEx2bb3in(b, a, c, d)
We thus obtain the following problem:
7:	T:
		(1, 2)              evalEx2start(a, b, c, d) -> evalEx2bb3in(b, a, c, d)
		(1, 1)              evalEx2entryin(a, b, c, d) -> evalEx2bb3in(b, a, c, d)
		(3*a + b + 2, 1)    evalEx2bb3in(a, b, c, d) -> evalEx2bbin(a, b, c, d) [ b >= 1 /\ a >= 1 ]
		(3*a + b + 2, 1)    evalEx2bbin(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1)
		(?, 1)              evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ 0 >= e + 1 ]
		(?, 1)              evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ e >= 1 ]
		(3*a + b + 2, 1)    evalEx2bb2in(a, b, c, d) -> evalEx2bb3in(c, d, c, d)
		(?, 1)              evalEx2bb1in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1)
	start location:	evalEx2start
	leaf cost:	3

Testing for reachability in the complexity graph removes the following transition from problem 7:
	evalEx2entryin(a, b, c, d) -> evalEx2bb3in(b, a, c, d)
We thus obtain the following problem:
8:	T:
		(?, 1)              evalEx2bb1in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1)
		(3*a + b + 2, 1)    evalEx2bb2in(a, b, c, d) -> evalEx2bb3in(c, d, c, d)
		(?, 1)              evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ e >= 1 ]
		(?, 1)              evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ 0 >= e + 1 ]
		(3*a + b + 2, 1)    evalEx2bbin(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1)
		(3*a + b + 2, 1)    evalEx2bb3in(a, b, c, d) -> evalEx2bbin(a, b, c, d) [ b >= 1 /\ a >= 1 ]
		(1, 2)              evalEx2start(a, b, c, d) -> evalEx2bb3in(b, a, c, d)
	start location:	evalEx2start
	leaf cost:	3

By chaining the transition evalEx2bb2in(a, b, c, d) -> evalEx2bb3in(c, d, c, d) with all transitions in problem 8, the following new transition is obtained:
	evalEx2bb2in(a, b, c, d) -> evalEx2bbin(c, d, c, d) [ d >= 1 /\ c >= 1 ]
We thus obtain the following problem:
9:	T:
		(3*a + b + 2, 2)    evalEx2bb2in(a, b, c, d) -> evalEx2bbin(c, d, c, d) [ d >= 1 /\ c >= 1 ]
		(?, 1)              evalEx2bb1in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1)
		(?, 1)              evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ e >= 1 ]
		(?, 1)              evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ 0 >= e + 1 ]
		(3*a + b + 2, 1)    evalEx2bbin(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1)
		(3*a + b + 2, 1)    evalEx2bb3in(a, b, c, d) -> evalEx2bbin(a, b, c, d) [ b >= 1 /\ a >= 1 ]
		(1, 2)              evalEx2start(a, b, c, d) -> evalEx2bb3in(b, a, c, d)
	start location:	evalEx2start
	leaf cost:	3

By chaining the transition evalEx2bb2in(a, b, c, d) -> evalEx2bbin(c, d, c, d) [ d >= 1 /\ c >= 1 ] with all transitions in problem 9, the following new transition is obtained:
	evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(c, d, c - 1, d - 1) [ d >= 1 /\ c >= 1 ]
We thus obtain the following problem:
10:	T:
		(3*a + b + 2, 3)    evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(c, d, c - 1, d - 1) [ d >= 1 /\ c >= 1 ]
		(?, 1)              evalEx2bb1in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1)
		(?, 1)              evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ e >= 1 ]
		(?, 1)              evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ 0 >= e + 1 ]
		(3*a + b + 2, 1)    evalEx2bbin(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1)
		(3*a + b + 2, 1)    evalEx2bb3in(a, b, c, d) -> evalEx2bbin(a, b, c, d) [ b >= 1 /\ a >= 1 ]
		(1, 2)              evalEx2start(a, b, c, d) -> evalEx2bb3in(b, a, c, d)
	start location:	evalEx2start
	leaf cost:	3

By chaining the transition evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ e >= 1 ] with all transitions in problem 10, the following new transition is obtained:
	evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1) [ e >= 1 ]
We thus obtain the following problem:
11:	T:
		(?, 2)              evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1) [ e >= 1 ]
		(3*a + b + 2, 3)    evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(c, d, c - 1, d - 1) [ d >= 1 /\ c >= 1 ]
		(?, 1)              evalEx2bb1in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1)
		(?, 1)              evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ 0 >= e + 1 ]
		(3*a + b + 2, 1)    evalEx2bbin(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1)
		(3*a + b + 2, 1)    evalEx2bb3in(a, b, c, d) -> evalEx2bbin(a, b, c, d) [ b >= 1 /\ a >= 1 ]
		(1, 2)              evalEx2start(a, b, c, d) -> evalEx2bb3in(b, a, c, d)
	start location:	evalEx2start
	leaf cost:	3

By chaining the transition evalEx2bb2in(a, b, c, d) -> evalEx2bb1in(a, b, c, d) [ 0 >= e + 1 ] with all transitions in problem 11, the following new transition is obtained:
	evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1) [ 0 >= e + 1 ]
We thus obtain the following problem:
12:	T:
		(?, 2)              evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1) [ 0 >= e + 1 ]
		(?, 2)              evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1) [ e >= 1 ]
		(3*a + b + 2, 3)    evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(c, d, c - 1, d - 1) [ d >= 1 /\ c >= 1 ]
		(?, 1)              evalEx2bb1in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1)
		(3*a + b + 2, 1)    evalEx2bbin(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1)
		(3*a + b + 2, 1)    evalEx2bb3in(a, b, c, d) -> evalEx2bbin(a, b, c, d) [ b >= 1 /\ a >= 1 ]
		(1, 2)              evalEx2start(a, b, c, d) -> evalEx2bb3in(b, a, c, d)
	start location:	evalEx2start
	leaf cost:	3

Testing for reachability in the complexity graph removes the following transition from problem 12:
	evalEx2bb1in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1)
We thus obtain the following problem:
13:	T:
		(?, 2)              evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1) [ 0 >= e + 1 ]
		(?, 2)              evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1) [ e >= 1 ]
		(3*a + b + 2, 3)    evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(c, d, c - 1, d - 1) [ d >= 1 /\ c >= 1 ]
		(3*a + b + 2, 1)    evalEx2bbin(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1)
		(3*a + b + 2, 1)    evalEx2bb3in(a, b, c, d) -> evalEx2bbin(a, b, c, d) [ b >= 1 /\ a >= 1 ]
		(1, 2)              evalEx2start(a, b, c, d) -> evalEx2bb3in(b, a, c, d)
	start location:	evalEx2start
	leaf cost:	3

By chaining the transition evalEx2bb3in(a, b, c, d) -> evalEx2bbin(a, b, c, d) [ b >= 1 /\ a >= 1 ] with all transitions in problem 13, the following new transition is obtained:
	evalEx2bb3in(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1) [ b >= 1 /\ a >= 1 ]
We thus obtain the following problem:
14:	T:
		(3*a + b + 2, 2)    evalEx2bb3in(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1) [ b >= 1 /\ a >= 1 ]
		(?, 2)              evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1) [ 0 >= e + 1 ]
		(?, 2)              evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1) [ e >= 1 ]
		(3*a + b + 2, 3)    evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(c, d, c - 1, d - 1) [ d >= 1 /\ c >= 1 ]
		(3*a + b + 2, 1)    evalEx2bbin(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1)
		(1, 2)              evalEx2start(a, b, c, d) -> evalEx2bb3in(b, a, c, d)
	start location:	evalEx2start
	leaf cost:	3

Testing for reachability in the complexity graph removes the following transition from problem 14:
	evalEx2bbin(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1)
We thus obtain the following problem:
15:	T:
		(?, 2)              evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1) [ 0 >= e + 1 ]
		(?, 2)              evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1) [ e >= 1 ]
		(3*a + b + 2, 3)    evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(c, d, c - 1, d - 1) [ d >= 1 /\ c >= 1 ]
		(3*a + b + 2, 2)    evalEx2bb3in(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1) [ b >= 1 /\ a >= 1 ]
		(1, 2)              evalEx2start(a, b, c, d) -> evalEx2bb3in(b, a, c, d)
	start location:	evalEx2start
	leaf cost:	3

By chaining the transition evalEx2start(a, b, c, d) -> evalEx2bb3in(b, a, c, d) with all transitions in problem 15, the following new transition is obtained:
	evalEx2start(a, b, c, d) -> evalEx2bb2in(b, a, b - 1, a - 1) [ a >= 1 /\ b >= 1 ]
We thus obtain the following problem:
16:	T:
		(1, 4)              evalEx2start(a, b, c, d) -> evalEx2bb2in(b, a, b - 1, a - 1) [ a >= 1 /\ b >= 1 ]
		(?, 2)              evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1) [ 0 >= e + 1 ]
		(?, 2)              evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1) [ e >= 1 ]
		(3*a + b + 2, 3)    evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(c, d, c - 1, d - 1) [ d >= 1 /\ c >= 1 ]
		(3*a + b + 2, 2)    evalEx2bb3in(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1) [ b >= 1 /\ a >= 1 ]
	start location:	evalEx2start
	leaf cost:	3

Testing for reachability in the complexity graph removes the following transition from problem 16:
	evalEx2bb3in(a, b, c, d) -> evalEx2bb2in(a, b, a - 1, b - 1) [ b >= 1 /\ a >= 1 ]
We thus obtain the following problem:
17:	T:
		(?, 2)              evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1) [ 0 >= e + 1 ]
		(?, 2)              evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(a, b, c + 1, d - 1) [ e >= 1 ]
		(3*a + b + 2, 3)    evalEx2bb2in(a, b, c, d) -> evalEx2bb2in(c, d, c - 1, d - 1) [ d >= 1 /\ c >= 1 ]
		(1, 4)              evalEx2start(a, b, c, d) -> evalEx2bb2in(b, a, b - 1, a - 1) [ a >= 1 /\ b >= 1 ]
	start location:	evalEx2start
	leaf cost:	3

Complexity upper bound ?

Time: 5.954 sec (SMT: 5.517 sec)