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

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

  ScanParameters(argc,argv);

  InitRandom();

  Saxiom=WithFml(Pos(Rel(ONE),True()),EMPTY_SEQUENT);
  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,"persat","axiom");
	PrintSequent(Saxiom,"deontic","axiom");
	PrintSequent(Sgoal,"result","conjecture");
      }
      else {
	fp=OpenFile(instance);
	FprintBanner(fp);
	FprintSequent(fp,S,"persat","axiom");
	FprintSequent(fp,Saxiom,"deontic","axiom");
	FprintSequent(fp,Sgoal,"result","conjecture");
	fclose(fp);
      }
    }
  }
  DeleteSequent(S);
  DeleteSequent(Sgoal);
  DeleteSequent(Saxiom);

  return 0;
}