YES(?, 1)

Initial complexity problem:
1:	T:
		(1, 1)    f0(a, b) -> f1(3000, b)
		(?, 1)    f1(a, b) -> f1(a, b + 1000) [ b + 889 >= 0 /\ 1999 >= a ]
	start location:	f0
	leaf cost:	0

Testing for reachability in the complexity graph removes the following transition from problem 1:
	f1(a, b) -> f1(a, b + 1000) [ b + 889 >= 0 /\ 1999 >= a ]
We thus obtain the following problem:
2:	T:
		(1, 1)    f0(a, b) -> f1(3000, b)
	start location:	f0
	leaf cost:	0

Complexity upper bound 1

Time: 0.017 sec (SMT: 0.016 sec)