function sylv(i)
	if i eq 1 then
		return 2;
	else
		return &*[sylv(j) : j in [1..i-1]]+1;
	end if;
end function;

function boundvolsimplex(i)
	if i eq 2 then
		return 9;
	else
		return 2*(sylv(i)-1)^2;
	end if;
end function;


procedure check(D)
  t:=#D;
  d:=D[1]+t-1;
  if (Factorial(&+[di : di in D])/&*[Factorial(di) : di in D])*&*[boundvolsimplex(di) : di in D] ge boundvolsimplex(d) then
    printf "d=%o t=%o D=%o\n",d,t,D;
  end if;
end procedure;

for i1 in [0..12] do
for i2 in [i1..12] do
for i3 in [i2..12] do
for i4 in [i3..12] do
for i5 in [i4..12] do
for i6 in [i5..12] do
for i7 in [i6..12] do
for i8 in [i7..12] do
for i9 in [i8..12] do
for i10 in [i9..12] do
for i11 in [i10..12] do
for i12 in [i11..12] do

D:=[i12,i11,i10,i9,i8,i7,i6,i5,i4,i3,i2,i1];
D:=[di : di in D | di gt 0];
if #D ge 2 and D[1]+#D-1 le 12 then
  if not (#D eq 2 and D[1] eq D[2]) then
    check(D);
  end if;
end if;

end for;
end for;
end for;
end for;
end for;
end for;
end for;
end for;
end for;
end for;
end for;
end for;

// RETURNS:
// d=4 t=2 D=[ 3, 2 ]
// d=5 t=2 D=[ 4, 3 ]
// d=4 t=3 D=[ 2, 2, 1 ]
// d=4 t=3 D=[ 2, 2, 2 ]
// d=5 t=3 D=[ 3, 3, 2 ]
// d=5 t=3 D=[ 3, 3, 3 ]
// d=6 t=3 D=[ 4, 4, 4 ]
// d=5 t=4 D=[ 2, 2, 2, 2 ]

// for such cases we still have to check what happens if the number of common vertices gets lower (or equiv. if d is bigger)

cases:=[[ 3, 2 ],[ 4, 3 ],[ 2, 2, 1 ],[ 2, 2, 2 ],[ 3, 3, 2 ],[ 3, 3, 3 ],[ 4, 4, 4 ],[ 2, 2, 2, 2 ]];

procedure second_check(D)
  t:=#D;
  d:=D[1]+t;
  if (Factorial(&+[di : di in D])/&*[Factorial(di) : di in D])*&*[boundvolsimplex(di) : di in D] ge boundvolsimplex(d) then
    printf "d=%o t=%o D=%o\n",d,t,D;
  end if;
end procedure;

for D in cases do second_check(D); end for;

// it does not return any more case.

