/******* MAIN ROUTINE ******/

int main(int argc, char *argv[])
{
  sequent S,Sgoal;
  integer instance;
  FILE *fp;

  ScanParameters(argc,argv);

  InitRandom();

  Sgoal=WithFml(False(),EMPTY_SEQUENT);

  S=EMPTY_SEQUENT;  
  for(instance=1; instance<=NthInstance; instance++) {
    DeleteSequent(S);
    S=GenerateFormulae();
    if (flag_Kenc || flag_S4enc)
      S=ModalizeFormulae(S);
    if (flag_all || instance==NthInstance) {
      if (flag_stdio) {
	PrintBanner();
	PrintSequent(S,"bound","hypothesis");
	PrintSequent(Sgoal,"result","conjecture");
      }
      else {
	fp=OpenFile(instance);
	FprintBanner(fp);
	FprintSequent(fp,S,"bound","hypothesis");
	FprintSequent(fp,Sgoal,"result","conjecture");
        fclose(fp);
      }
    }
  }
  DeleteSequent(S);
  DeleteSequent(Sgoal);

  return 0;
}