#define MAXBANNER 10
char *banner[MAXBANNER+1] = {
  "Unbounded Modal Sat from QBF with Inverse - Randomly Generated",
  "Extended from Ladner, SIAM JOC, 1977, SIAM Press by F. Massacci",
  "Smart coding avoid the auxiliary variables of the original paper",
  "With ladner flag encoding further optimized",
  "With sss flag enc. extended from Schimdt-Schauss Smolka, AIJ 1991, Elsev.",
  "With K,S4 flag prop variables hidden by modal proposition for K and S4",
  "(formulae are no longer in CNF) due to Halpern, AIJ 95, Elsevier",
  "Parameter depth=-1 generate a random number of alternations",
  "Benchmark generator by Fabio Massacci (massacci@dis.uniroma1.it)",
  "Copyright Fabio Massacci, November 1999"
};

char *name="qbf-inv";

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

integer MaxVariables=2;
integer MaxClauses=20;
integer MaxDepth=2;
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;