code: package wprover;
  
  import gprover.Prover;
  
  import javax.swing.*;
  import java.awt.event.ActionListener;
  import java.awt.event.ActionEvent;
  
  public class GProver implements Runnable {
  
      GExpert gxInstance;
      PanelProve1 pprove;
      Thread main;
      private int Status = 0;
      private boolean isRunning = false;
  
      Timer timer = null;
      int number = 0;
      long ftime = 0;
  
      public GProver(PanelProve1 p, GExpert fr) {
          pprove = p;
          gxInstance = fr;
      }
  
      public void setFix() {
          Status = 0;
      }
  
      public void setProve() {
          Status = 1;
      }
  
      public void startTimer() {
          number = 0;
          ftime = System.currentTimeMillis();
  
          timer = new Timer(100, new ActionListener() {
              public void actionPerformed(ActionEvent e) {
                 // int n = Prover.getNumberofProperties();
                  if (!isRunning)
                      timer.stop();
                  else {
                      double t = System.currentTimeMillis() - ftime;
                      int ft = (int) (t / 1000);
                      gxInstance.setLabelText2("Building fixpoint (" + ft + " seconds"
                              + ";  " + Prover.getNumberofProperties() + " facts)");
                  }
              }
          });
          timer.start();
      }
  
      public void run() {
          isRunning = true;
          try {
              if (Status == 0) {
                  long n1 = System.currentTimeMillis();
                  Prover.run();
                  n1 = System.currentTimeMillis() - n1;
                  pprove.displayDatabase(n1);
              } else {
                  boolean t = Prover.prove();
                  pprove.displayGDDProve(t);
              }
          } catch (OutOfMemoryError ee) {
              if (CMisc.DEBUG)
                  ee.printStackTrace();
              CMisc.print(ee.getMessage());
              if (gxInstance != null)
                  gxInstance.setTextLabel2("System run out of memory!", -1);
              Prover.reset();
              isRunning = false;
              JOptionPane.showMessageDialog(gxInstance,
                      "System run out of memory!\n The theorem is not proved.",
                      "Not Proved", JOptionPane.WARNING_MESSAGE);
  
          } catch (Error ee) {
              JOptionPane.showMessageDialog(gxInstance,
                      "The theorem is not proved.\n" + ee.getMessage(),
                      "Not Proved", JOptionPane.WARNING_MESSAGE);
              Prover.reset();
  
          } catch (Exception ee) {
              JOptionPane.showMessageDialog(gxInstance,
                      "The theorem is not proved.\n" + ee.getMessage(),
                      "Not Proved", JOptionPane.WARNING_MESSAGE);
              Prover.reset();
          }
          if (gxInstance != null)
              gxInstance.stopTimer();
  
          isRunning = false;
      }
  
      public void start() {
          if (isRunning) return;
          main = new Thread(this, "Prover");
          main.start();
          startTimer();
      }
  
      public boolean isRunning() {
          return isRunning;
      }
  }
  
  