/******* BENCHMARK DESCRIPTION ******/
#define MAXBANNER 7
char *banner[MAXBANNER+1] = {
  "Unbounded Modal Sat for S5n - Randomly Generated",
  "Original reference Ladner, SIAM J. of Comp., SIAM Press",
  "Smart coding avoid the auxiliary variables of the original paper",
  "Parameter depth=-1 generate a random number of alternations",
  "With K,S4 flag prop variables hidden by modal proposition for K and S4",
  "Benchmark generator by Fabio Massacci (massacci@dis.uniroma1.it)", 
  "Copyright Fabio Massacci, November 1998"
};

char *name="qbf-S5n";

/******* BENCHMARK PARAMETERS ******/

integer MaxVariables=2;
integer MaxClauses=16;
integer MaxDepth=3;
integer MaxLiterals=4;
real  ProbModal=0.5;
real  ProbNegated=0.5;
bool flag_Kenc=0;
bool flag_S4enc=0;
bool flag_LadnerEnc=0;
bool flag_SSSEnc=0;

#define AltDepth (MaxVariables*(MaxDepth+1))

/******* OPTIONAL PARAMETERS ******/
bool flag_test=1;
bool flag_stdio=0;
bool flag_all=0;
integer NthInstance=1;
integer MaxFailures=(integer)TWO_TO_THE_24;