/*@ logic int pow(int x, int n) */

//@ type int3

/*@ logic int3 prod3(int x1, int x2, int x3) */

/*@ predicate reachable_(int base, int c2, int c1, int c0) */

/*@ ensures \result == 3 * pow(2, 3 * pow(2, pow(3, 3)) + pow(3, 3)) - 1 */
int main(void) 
{
  int c2 = 2;
  int c1 = 2;
  int c0 = 2;
  int base;
  /*@ invariant 0 <= c0 && 0 <= c1 && 0 <= c2 && 0 <= base &&
      reachable_(base,c2,c1,c0)
      variant prod3(c2,c1,c0) for lex3 */
  for(base = 3; 1 ; base++)
    {
      if (0 < c0)
	c0--;
      else if (0 < c1)
	{
	  c1--;
	  c0 = base;
	}
      else if (0 < c2)
	{
	  c2--;
	  c0 = c1 = base;
	}
      else break;
    }
  return base;
}