/******* BENCHMARK DESCRIPTION ******/

#define MAXBANNER 7
char *banner[MAXBANNER] = {
  "Bounded (Modalized) Formulae in CNF - Randomly Generated",
  "Refined version from Giunchiglia & Sebastiani, CADE-96, Springer Verlag",
  "and Hustadt & Schmidt, IJCAI-97, Morgan Kaufman",
  "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",
  "Benchmark generator by Fabio Massacci (massacci@dis.uniroma1.it)", 
  "Copyright Fabio Massacci, November 1998"
};

char *name="bound";

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

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

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