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

Initial complexity problem:
1:	T:
		(1, 1)    l0(a, b) -> l1(a, b)
		(?, 1)    l1(a, b) -> l1(a - 1, b + 1) [ a >= 1 ]
		(?, 1)    l1(a, b) -> l2(a, b) [ 0 >= a ]
		(?, 1)    l2(a, b) -> l2(a, b - 1) [ b >= 1 ]
	start location:	l0
	leaf cost:	0

A polynomial rank function with
	Pol(l0) = 1
	Pol(l1) = 1
	Pol(l2) = -1
orients all transitions weakly and the transition
	l1(a, b) -> l2(a, b) [ 0 >= a ]
strictly and produces the following problem:
2:	T:
		(1, 1)    l0(a, b) -> l1(a, b)
		(?, 1)    l1(a, b) -> l1(a - 1, b + 1) [ a >= 1 ]
		(1, 1)    l1(a, b) -> l2(a, b) [ 0 >= a ]
		(?, 1)    l2(a, b) -> l2(a, b - 1) [ b >= 1 ]
	start location:	l0
	leaf cost:	0

A polynomial rank function with
	Pol(l0) = V_1
	Pol(l1) = V_1
	Pol(l2) = V_1
orients all transitions weakly and the transition
	l1(a, b) -> l1(a - 1, b + 1) [ a >= 1 ]
strictly and produces the following problem:
3:	T:
		(1, 1)    l0(a, b) -> l1(a, b)
		(a, 1)    l1(a, b) -> l1(a - 1, b + 1) [ a >= 1 ]
		(1, 1)    l1(a, b) -> l2(a, b) [ 0 >= a ]
		(?, 1)    l2(a, b) -> l2(a, b - 1) [ b >= 1 ]
	start location:	l0
	leaf cost:	0

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

Complexity upper bound 2*a + b + 2

Time: 0.170 sec (SMT: 0.160 sec)