code: package gprover;
  
  import java.io.*;
  import java.util.Vector;
  
  
  /**
   * Created by IntelliJ IDEA.
   * User: Ye
   * Date: 2006-2-15
   * Time: 17:20:04
   * To change this template use File | Settings | File Templates.
   */
  public class Main {
      public static void main1(String[] args) {
          try {
  
              String user_directory = System.getProperty("user.dir");
              String sp = System.getProperty("file.separator");
              String dr = user_directory + sp + "ex";
              File file = new File(dr);
  
  
              Vector vm = new Vector();
              readThems(file, vm);
              for (int id = 0; id < vm.size(); id++) {
                  gterm gt = (gterm) vm.get(id);
                  System.out.print(id + " : " + gt.getName() + "\t\t");
                  if (id % 4 == 0)
                      Cm.print("\n");
              }
  
              int t = 0;
              int f = 0;
              int n = 0;
              Cm.print("\n\n************************\n");
  
              Vector tlist = new Vector();
              long t1 = System.currentTimeMillis();
  
              for (int id = 0; id < vm.size(); id++) {
                  gdd_bc db = new gdd_bc();
                  db.init_dbase();
  
                  gterm gt = (gterm) vm.get(id);
                  db.setExample(gt);
  
                  db.sbase();
                  db.fixpoint();
  
                  if (gt.getConc().pred == 0) {
                      n++;
                      System.out.print(id + " : " + gt.getName() + "\t\tNO\n");
                  } else if (db.docc()) {
                      t++;
                      System.out.print(id + " : " + gt.getName() + "\t\ttrue\n");
                      tlist.add(gt);
  
                      FileOutputStream fp;
                      String drec = (dr + sp + "proved");
                      File ff = new File(drec + sp + gt.getName() + ".rtf");
  
                      if (ff.exists()) {
                          ff.delete();
                          fp = new FileOutputStream(ff, true);
  
                      } else {
                          ff.createNewFile();
                          fp = new FileOutputStream(ff, false);
                      }
                      if (fp == null) return;
                      DataOutputStream out = new DataOutputStream(fp);
                      gt.Save(out);
  
                      //db.setPrintToString();
                      //db.show_fproof();
                      //out.writeBytes(db.getFileProve().append("\n********************************\n").toString());
                      out.close();
                  } else {
                      f++;
                      System.out.print(id + " : " + gt.getName() + "\t\tfalse\n");
                  }
              }
              Cm.print("Total = " + vm.size() + ";  t =  " + t + ",  f = " + f + ", n = " + n);
              long t2 = System.currentTimeMillis();
              Cm.print("Time = " + (t2 - t1) / 1000.0);
          } catch (IOException ee) {
          }
      }
  
      static void proveGDD(gterm gt) {
  
      }
  
      public static void main(String[] args) {
          main1(args);
      }
  
      static void proveFull() {
          try {
              String user_directory = System.getProperty("user.dir");
              String sp = System.getProperty("file.separator");
              String dr = user_directory + sp + "ex";
              File file = new File(dr);
  
  
              Vector vm = new Vector();
              readThems(file, vm);
              for (int id = 0; id < vm.size(); id++) {
                  gterm gt = (gterm) vm.get(id);
                  System.out.print(id + " : " + gt.getName() + "\t\t");
                  if (id % 4 == 0)
                      Cm.print("\n");
  
  
              }
  
              int t = 0;
              int f = 0;
              int n = 0;
              Cm.print("\n\n************************\n");
  
              Vector tlist = new Vector();
              long t1 = System.currentTimeMillis();
              Full full = new Full();
              int nt = 0;
              for (int id = 0; id < vm.size(); id++) {
                  Full.set_showdetai(false);
  
  
                  full.init_dbase();
  
                  gterm gt = (gterm) vm.get(id);
                  full.setExample(gt);
                  full.sbase();
                  full.setNoPrint();
  
                  if (id == 482) {
                      System.gc();
                  }
                  full.prove_full();
                  if (full.isProvedTrue()) {
                      FileOutputStream fp;
                      String drec = (dr + sp + "proved");
                      File ff = new File(drec + sp + gt.getName() + ".rtf");
  
                      if (ff.exists()) {
                          ff.delete();
                          fp = new FileOutputStream(ff, true);
  
                      } else {
                          ff.createNewFile();
                          fp = new FileOutputStream(ff, false);
                      }
                      if (fp == null) return;
                      DataOutputStream out = new DataOutputStream(fp);
  
                      boolean s = false;
                      gr_term gr = full.getFullAngleProofHead();
                      while (gr != null) {
                          el_term e = gr.el;
                          if (e == null) {
                              gr = gr.nx;
                              continue;
                          }
                          while (e != null) {
                              cond c = e.co;
                              full.setPrintToString();
                              while (c != null) {
                                  full.setConc(c);
                                  if (full.docc()) {
                                      full.show_fproof();
                                      cond conc = full.all_nd.nx;
                                      int nx = 0;
                                      while (conc != null) {
                                          nx++;
                                          conc = conc.nx;
                                      }
                                      if (nx > 1) {
                                          s = true;
                                          System.out.print("(" + nx + ")");
                                          //   full.show_fproof();
                                          out.writeBytes(full.getFileProve().append("\n********************************\n").toString());
                                      }
                                  }
                                  c = c.nx;
                              }
                              e = e.nx;
                          }
                          gr = gr.nx;
  
                      }
                      if (s) {
                          gt.Save(out);
                      }
                      out.close();
                      nt ++;
                      System.out.print(id + " : " + gt.getName() + "\t\ttrue\n");
  
                  } else {
                      // System.out.print(id + " : " + gt.getName() + "\t\tfalse\n");
                  }
              }
              Cm.print("Total :" +vm.size() +", and true: " +nt);
          } catch (IOException ee) {
  
          }
  
      }
  
      static void readThems(File file, Vector v) throws IOException {
          File[] sf = file.listFiles(new FileFilter() {
              public boolean accept(File pathname) {
                  String nm = pathname.getName();
                  return !(nm.contains("."));
              }
  
          });
          for (int i = 0; i < sf.length; i++) {
              if (sf[i].isDirectory())
                  readThems(sf[i], v);
              else {
                  BufferedReader in = new BufferedReader(new FileReader(sf[i]));
  
                  while (true) {
                      gterm tm = new gterm();
                      if (!tm.readAterm(in)) break;
                      tm.setName(sf[i].getName());
                      v.add(tm);
                  }
                  in.close();
              }
          }
      }
  
  
      static int inputInt() throws IOException {
          byte[] bm = new byte[10];
          System.in.read(bm);
          String sid = new String(bm).trim();
          int dd = Integer.parseInt(sid);
          return dd;
      }
  }
  