YES(?, 5*b + 2*b^2 + 2)

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

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

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

A polynomial rank function with
	Pol(l3) = 2*V_3 - 1
	Pol(l2) = 2*V_3
and size complexities
	S("l3(a, b, c, d) -> l2(a, b, c - 1, d) [ 0 >= d /\\ c >= 1 ]", 0-0) = b
	S("l3(a, b, c, d) -> l2(a, b, c - 1, d) [ 0 >= d /\\ c >= 1 ]", 0-1) = b
	S("l3(a, b, c, d) -> l2(a, b, c - 1, d) [ 0 >= d /\\ c >= 1 ]", 0-2) = b
	S("l3(a, b, c, d) -> l2(a, b, c - 1, d) [ 0 >= d /\\ c >= 1 ]", 0-3) = b
	S("l3(a, b, c, d) -> l3(a, b, c, d - 1) [ d >= 1 /\\ c >= 1 ]", 0-0) = b
	S("l3(a, b, c, d) -> l3(a, b, c, d - 1) [ d >= 1 /\\ c >= 1 ]", 0-1) = b
	S("l3(a, b, c, d) -> l3(a, b, c, d - 1) [ d >= 1 /\\ c >= 1 ]", 0-2) = b
	S("l3(a, b, c, d) -> l3(a, b, c, d - 1) [ d >= 1 /\\ c >= 1 ]", 0-3) = b
	S("l2(a, b, c, d) -> l3(a, b, c, c) [ c >= 1 ]", 0-0) = b
	S("l2(a, b, c, d) -> l3(a, b, c, c) [ c >= 1 ]", 0-1) = b
	S("l2(a, b, c, d) -> l3(a, b, c, c) [ c >= 1 ]", 0-2) = b
	S("l2(a, b, c, d) -> l3(a, b, c, c) [ c >= 1 ]", 0-3) = b
	S("l1(a, b, c, d) -> l2(a, b, a, d) [ 0 >= b ]", 0-0) = b
	S("l1(a, b, c, d) -> l2(a, b, a, d) [ 0 >= b ]", 0-1) = b
	S("l1(a, b, c, d) -> l2(a, b, a, d) [ 0 >= b ]", 0-2) = b
	S("l1(a, b, c, d) -> l2(a, b, a, d) [ 0 >= b ]", 0-3) = d
	S("l1(a, b, c, d) -> l1(a + 1, b - 1, c, d) [ b >= 1 ]", 0-0) = b
	S("l1(a, b, c, d) -> l1(a + 1, b - 1, c, d) [ b >= 1 ]", 0-1) = b
	S("l1(a, b, c, d) -> l1(a + 1, b - 1, c, d) [ b >= 1 ]", 0-2) = c
	S("l1(a, b, c, d) -> l1(a + 1, b - 1, c, d) [ b >= 1 ]", 0-3) = d
	S("l0(a, b, c, d) -> l1(0, b, c, d)", 0-0) = 0
	S("l0(a, b, c, d) -> l1(0, b, c, d)", 0-1) = b
	S("l0(a, b, c, d) -> l1(0, b, c, d)", 0-2) = c
	S("l0(a, b, c, d) -> l1(0, b, c, d)", 0-3) = d
orients the transitions
	l3(a, b, c, d) -> l3(a, b, c, d - 1) [ d >= 1 /\ c >= 1 ]
	l3(a, b, c, d) -> l2(a, b, c - 1, d) [ 0 >= d /\ c >= 1 ]
	l2(a, b, c, d) -> l3(a, b, c, c) [ c >= 1 ]
weakly and the transitions
	l3(a, b, c, d) -> l2(a, b, c - 1, d) [ 0 >= d /\ c >= 1 ]
	l2(a, b, c, d) -> l3(a, b, c, c) [ c >= 1 ]
strictly and produces the following problem:
4:	T:
		(1, 1)      l0(a, b, c, d) -> l1(0, b, c, d)
		(b, 1)      l1(a, b, c, d) -> l1(a + 1, b - 1, c, d) [ b >= 1 ]
		(1, 1)      l1(a, b, c, d) -> l2(a, b, a, d) [ 0 >= b ]
		(2*b, 1)    l2(a, b, c, d) -> l3(a, b, c, c) [ c >= 1 ]
		(?, 1)      l3(a, b, c, d) -> l3(a, b, c, d - 1) [ d >= 1 /\ c >= 1 ]
		(2*b, 1)    l3(a, b, c, d) -> l2(a, b, c - 1, d) [ 0 >= d /\ c >= 1 ]
	start location:	l0
	leaf cost:	0

A polynomial rank function with
	Pol(l3) = V_4
and size complexities
	S("l3(a, b, c, d) -> l2(a, b, c - 1, d) [ 0 >= d /\\ c >= 1 ]", 0-0) = b
	S("l3(a, b, c, d) -> l2(a, b, c - 1, d) [ 0 >= d /\\ c >= 1 ]", 0-1) = b
	S("l3(a, b, c, d) -> l2(a, b, c - 1, d) [ 0 >= d /\\ c >= 1 ]", 0-2) = b
	S("l3(a, b, c, d) -> l2(a, b, c - 1, d) [ 0 >= d /\\ c >= 1 ]", 0-3) = b
	S("l3(a, b, c, d) -> l3(a, b, c, d - 1) [ d >= 1 /\\ c >= 1 ]", 0-0) = b
	S("l3(a, b, c, d) -> l3(a, b, c, d - 1) [ d >= 1 /\\ c >= 1 ]", 0-1) = b
	S("l3(a, b, c, d) -> l3(a, b, c, d - 1) [ d >= 1 /\\ c >= 1 ]", 0-2) = b
	S("l3(a, b, c, d) -> l3(a, b, c, d - 1) [ d >= 1 /\\ c >= 1 ]", 0-3) = b
	S("l2(a, b, c, d) -> l3(a, b, c, c) [ c >= 1 ]", 0-0) = b
	S("l2(a, b, c, d) -> l3(a, b, c, c) [ c >= 1 ]", 0-1) = b
	S("l2(a, b, c, d) -> l3(a, b, c, c) [ c >= 1 ]", 0-2) = b
	S("l2(a, b, c, d) -> l3(a, b, c, c) [ c >= 1 ]", 0-3) = b
	S("l1(a, b, c, d) -> l2(a, b, a, d) [ 0 >= b ]", 0-0) = b
	S("l1(a, b, c, d) -> l2(a, b, a, d) [ 0 >= b ]", 0-1) = b
	S("l1(a, b, c, d) -> l2(a, b, a, d) [ 0 >= b ]", 0-2) = b
	S("l1(a, b, c, d) -> l2(a, b, a, d) [ 0 >= b ]", 0-3) = d
	S("l1(a, b, c, d) -> l1(a + 1, b - 1, c, d) [ b >= 1 ]", 0-0) = b
	S("l1(a, b, c, d) -> l1(a + 1, b - 1, c, d) [ b >= 1 ]", 0-1) = b
	S("l1(a, b, c, d) -> l1(a + 1, b - 1, c, d) [ b >= 1 ]", 0-2) = c
	S("l1(a, b, c, d) -> l1(a + 1, b - 1, c, d) [ b >= 1 ]", 0-3) = d
	S("l0(a, b, c, d) -> l1(0, b, c, d)", 0-0) = 0
	S("l0(a, b, c, d) -> l1(0, b, c, d)", 0-1) = b
	S("l0(a, b, c, d) -> l1(0, b, c, d)", 0-2) = c
	S("l0(a, b, c, d) -> l1(0, b, c, d)", 0-3) = d
orients the transition
	l3(a, b, c, d) -> l3(a, b, c, d - 1) [ d >= 1 /\ c >= 1 ]
weakly and the transition
	l3(a, b, c, d) -> l3(a, b, c, d - 1) [ d >= 1 /\ c >= 1 ]
strictly and produces the following problem:
5:	T:
		(1, 1)        l0(a, b, c, d) -> l1(0, b, c, d)
		(b, 1)        l1(a, b, c, d) -> l1(a + 1, b - 1, c, d) [ b >= 1 ]
		(1, 1)        l1(a, b, c, d) -> l2(a, b, a, d) [ 0 >= b ]
		(2*b, 1)      l2(a, b, c, d) -> l3(a, b, c, c) [ c >= 1 ]
		(2*b^2, 1)    l3(a, b, c, d) -> l3(a, b, c, d - 1) [ d >= 1 /\ c >= 1 ]
		(2*b, 1)      l3(a, b, c, d) -> l2(a, b, c - 1, d) [ 0 >= d /\ c >= 1 ]
	start location:	l0
	leaf cost:	0

Complexity upper bound 5*b + 2*b^2 + 2

Time: 0.298 sec (SMT: 0.281 sec)