/******* MAIN FILE ******/

int main(int argc, char *argv[])
{
  sequent QBFS,ModS,AltS,Sgoal;
  integer instance;
  int i;
  FILE *fp;

  ScanParameters(argc,argv);

  InitRandom();

  Sgoal=WithFml(False(),EMPTY_SEQUENT);

  MaxDepth=FindWorkableDepth(MaxDepth,MaxVariables);
    
  QBFS=EMPTY_SEQUENT;
  ModS=EMPTY_SEQUENT;
  AltS=EMPTY_SEQUENT;
  for(instance=1; instance<=NthInstance; instance++) {
    DeleteSequent(QBFS);
    DeleteSequent(ModS);
    DeleteSequent(AltS);

    QBFS=GenerateQuantifiedFormulae();
    ModS=GenerateModalFormulae(QBFS);
    AltS=GenerateAltFormulae(QBFS);

    if (flag_Kenc || flag_S4enc) {
      ModS=ModalizeFormulae(ModS);
      AltS=ModalizeFormulae(AltS);
    }
    if (flag_all || instance==NthInstance) {
      if (flag_stdio) {
	PrintBanner();
	PrintSequent(ModS,"mod","hypothesis");
	PrintSequent(AltS,"alt","hypothesis");
	PrintSequent(Sgoal,"result","conjecture");
      }
      else {
	fp=OpenFile(instance);
	FprintBanner(fp);
	FprintSequent(fp,ModS,"mod","hypothesis");
	FprintSequent(fp,AltS,"alt","hypothesis");
	FprintSequent(fp,Sgoal,"result","conjecture");
	fclose(fp);
      }
    }
  }


  DeleteSequent(QBFS);
  DeleteSequent(ModS);
  DeleteSequent(AltS);
  DeleteSequent(Sgoal);

  return 0;
}