#define MAXBANNER 5
char *banner[MAXBANNER+1] = {
  "Periodic Satisfiability in CNF with Inverse - Randomly Generated",
  "Original reference Orlin, STOC 81, ACM Press",
  "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="psat-inv";

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

integer MaxVariables=4;
integer MaxClauses=32;
integer MaxDepth=1;
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;

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