YES(?, a + 1)

Initial complexity problem:
1:	T:
		(?, 1)    zip3(a, b, c) -> zip3(a - 1, b - 1, c - 1) [ a >= 1 /\ b >= 1 /\ c >= 1 ]
		(?, 1)    group3(a, b, c) -> group3(a - 3, b, c) [ a >= 4 ]
		(1, 1)    start(a, b, c) -> zip3(a, b, c)
	start location:	start
	leaf cost:	0

Testing for reachability in the complexity graph removes the following transition from problem 1:
	group3(a, b, c) -> group3(a - 3, b, c) [ a >= 4 ]
We thus obtain the following problem:
2:	T:
		(?, 1)    zip3(a, b, c) -> zip3(a - 1, b - 1, c - 1) [ a >= 1 /\ b >= 1 /\ c >= 1 ]
		(1, 1)    start(a, b, c) -> zip3(a, b, c)
	start location:	start
	leaf cost:	0

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

Complexity upper bound a + 1

Time: 0.155 sec (SMT: 0.149 sec)