YES(?, 3)

Initial complexity problem:
1:	T:
		(?, 1)    f2(a, b, c, d) -> f2(a + 1, b + 1, c - 1, d)
		(1, 1)    f1(a, b, c, d) -> f2(a, b, c, d) [ a >= c /\ b >= a + 1 /\ c >= b + 1 ]
		(1, 1)    f1(a, b, c, d) -> f300(a, b, c, e) [ c >= b + 1 /\ b >= a + 1 /\ c >= a + 1 ]
		(1, 1)    f1(a, b, c, d) -> f300(a, b, c, e) [ b >= a + 1 /\ b >= c ]
		(1, 1)    f1(a, b, c, d) -> f300(a, b, c, e) [ a >= b ]
	start location:	f1
	leaf cost:	0

Testing for unsatisfiable constraints removes the following transition from problem 1:
	f1(a, b, c, d) -> f2(a, b, c, d) [ a >= c /\ b >= a + 1 /\ c >= b + 1 ]
We thus obtain the following problem:
2:	T:
		(?, 1)    f2(a, b, c, d) -> f2(a + 1, b + 1, c - 1, d)
		(1, 1)    f1(a, b, c, d) -> f300(a, b, c, e) [ c >= b + 1 /\ b >= a + 1 /\ c >= a + 1 ]
		(1, 1)    f1(a, b, c, d) -> f300(a, b, c, e) [ b >= a + 1 /\ b >= c ]
		(1, 1)    f1(a, b, c, d) -> f300(a, b, c, e) [ a >= b ]
	start location:	f1
	leaf cost:	0

Testing for reachability in the complexity graph removes the following transition from problem 2:
	f2(a, b, c, d) -> f2(a + 1, b + 1, c - 1, d)
We thus obtain the following problem:
3:	T:
		(1, 1)    f1(a, b, c, d) -> f300(a, b, c, e) [ a >= b ]
		(1, 1)    f1(a, b, c, d) -> f300(a, b, c, e) [ b >= a + 1 /\ b >= c ]
		(1, 1)    f1(a, b, c, d) -> f300(a, b, c, e) [ c >= b + 1 /\ b >= a + 1 /\ c >= a + 1 ]
	start location:	f1
	leaf cost:	0

Complexity upper bound 3

Time: 0.057 sec (SMT: 0.054 sec)