YES(?, 2*a + 2*b + 2)

Initial complexity problem:
1:	T:
		(?, 1)    eval(a, b) -> eval(a, b + 1) [ a >= b + 1 ]
		(?, 1)    eval(a, b) -> eval(a, b + 1) [ b >= a + 1 /\ a >= b + 1 ]
		(?, 1)    eval(a, b) -> eval(a + 1, b) [ a >= b + 1 /\ b >= a ]
		(?, 1)    eval(a, b) -> eval(a + 1, b) [ b >= a + 1 /\ b >= a ]
		(1, 1)    start(a, b) -> eval(a, b)
	start location:	start
	leaf cost:	0

Testing for unsatisfiable constraints removes the following transitions from problem 1:
	eval(a, b) -> eval(a, b + 1) [ b >= a + 1 /\ a >= b + 1 ]
	eval(a, b) -> eval(a + 1, b) [ a >= b + 1 /\ b >= a ]
We thus obtain the following problem:
2:	T:
		(?, 1)    eval(a, b) -> eval(a, b + 1) [ a >= b + 1 ]
		(?, 1)    eval(a, b) -> eval(a + 1, b) [ b >= a + 1 /\ b >= a ]
		(1, 1)    start(a, b) -> eval(a, b)
	start location:	start
	leaf cost:	0

A polynomial rank function with
	Pol(eval) = V_1 - V_2
and size complexities
	S("start(a, b) -> eval(a, b)", 0-0) = a
	S("start(a, b) -> eval(a, b)", 0-1) = b
	S("eval(a, b) -> eval(a + 1, b) [ b >= a + 1 /\\ b >= a ]", 0-0) = ?
	S("eval(a, b) -> eval(a + 1, b) [ b >= a + 1 /\\ b >= a ]", 0-1) = b
	S("eval(a, b) -> eval(a, b + 1) [ a >= b + 1 ]", 0-0) = a
	S("eval(a, b) -> eval(a, b + 1) [ a >= b + 1 ]", 0-1) = ?
orients the transition
	eval(a, b) -> eval(a, b + 1) [ a >= b + 1 ]
weakly and the transition
	eval(a, b) -> eval(a, b + 1) [ a >= b + 1 ]
strictly and produces the following problem:
3:	T:
		(a + b, 1)    eval(a, b) -> eval(a, b + 1) [ a >= b + 1 ]
		(?, 1)        eval(a, b) -> eval(a + 1, b) [ b >= a + 1 /\ b >= a ]
		(1, 1)        start(a, b) -> eval(a, b)
	start location:	start
	leaf cost:	0

A polynomial rank function with
	Pol(eval) = -V_1 + V_2 + 1
and size complexities
	S("start(a, b) -> eval(a, b)", 0-0) = a
	S("start(a, b) -> eval(a, b)", 0-1) = b
	S("eval(a, b) -> eval(a + 1, b) [ b >= a + 1 /\\ b >= a ]", 0-0) = ?
	S("eval(a, b) -> eval(a + 1, b) [ b >= a + 1 /\\ b >= a ]", 0-1) = b
	S("eval(a, b) -> eval(a, b + 1) [ a >= b + 1 ]", 0-0) = a
	S("eval(a, b) -> eval(a, b + 1) [ a >= b + 1 ]", 0-1) = 2*a + 2*b
orients the transition
	eval(a, b) -> eval(a + 1, b) [ b >= a + 1 /\ b >= a ]
weakly and the transition
	eval(a, b) -> eval(a + 1, b) [ b >= a + 1 /\ b >= a ]
strictly and produces the following problem:
4:	T:
		(a + b, 1)        eval(a, b) -> eval(a, b + 1) [ a >= b + 1 ]
		(a + b + 1, 1)    eval(a, b) -> eval(a + 1, b) [ b >= a + 1 /\ b >= a ]
		(1, 1)            start(a, b) -> eval(a, b)
	start location:	start
	leaf cost:	0

Complexity upper bound 2*a + 2*b + 2

Time: 0.150 sec (SMT: 0.141 sec)