YES(?, 16*a + 6*b + 10*c + 10)

Initial complexity problem:
1:	T:
		(?, 1)    eval1(a, b, c) -> eval2(a, b, c) [ a >= b + 1 ]
		(?, 1)    eval2(a, b, c) -> eval1(a, b + 1, c) [ a >= c + 1 ]
		(?, 1)    eval2(a, b, c) -> eval1(a, b, c + 1) [ a >= c + 1 ]
		(?, 1)    eval2(a, b, c) -> eval1(a - 1, b, c) [ c >= a ]
		(1, 1)    start(a, b, c) -> eval1(a, b, c)
	start location:	start
	leaf cost:	0

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

Applied AI with 'oct' on problem 2 to obtain the following invariants:
  For symbol eval2: X_1 - X_2 - 1 >= 0


This yielded the following problem:
3:	T:
		(1, 1)                start(a, b, c) -> eval1(a, b, c)
		(?, 1)                eval2(a, b, c) -> eval1(a - 1, b, c) [ a - b - 1 >= 0 /\ c >= a ]
		(2*a + 2*c + 1, 1)    eval2(a, b, c) -> eval1(a, b, c + 1) [ a - b - 1 >= 0 /\ a >= c + 1 ]
		(?, 1)                eval2(a, b, c) -> eval1(a, b + 1, c) [ a - b - 1 >= 0 /\ a >= c + 1 ]
		(?, 1)                eval1(a, b, c) -> eval2(a, b, c) [ a >= b + 1 ]
	start location:	start
	leaf cost:	0

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

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

Repeatedly propagating knowledge in problem 5 produces the following problem:
6:	T:
		(1, 1)                      start(a, b, c) -> eval1(a, b, c)
		(a + b, 1)                  eval2(a, b, c) -> eval1(a - 1, b, c) [ a - b - 1 >= 0 /\ c >= a ]
		(2*a + 2*c + 1, 1)          eval2(a, b, c) -> eval1(a, b, c + 1) [ a - b - 1 >= 0 /\ a >= c + 1 ]
		(5*a + 2*b + 3*c + 3, 1)    eval2(a, b, c) -> eval1(a, b + 1, c) [ a - b - 1 >= 0 /\ a >= c + 1 ]
		(8*a + 3*b + 5*c + 5, 1)    eval1(a, b, c) -> eval2(a, b, c) [ a >= b + 1 ]
	start location:	start
	leaf cost:	0

Complexity upper bound 16*a + 6*b + 10*c + 10

Time: 0.299 sec (SMT: 0.282 sec)