//Robert Swartz
//Meta Theorem
//Copyright 2025
//Processor Design Capability


import java.awt.*;
import java.awt.datatransfer.*;
import java.awt.event.*;
import java.io.*;
import java.util.*;


public class MetaTheorem
{
   public static void main(String[] args)
   {
      AppletImage metaApplet = new AppletImage();
      int w = 1190, h = 730, h2 = 75;
      metaApplet.pF.setLocation(200, 200);
      metaApplet.pF.setVisible(true);
      metaApplet.pF.setSize(w, h);
      metaApplet.pF.setResizable(false);
      metaApplet.mwa = new MyWindowAdapter(metaApplet);
      metaApplet.pF.addWindowListener(metaApplet.mwa);
      metaApplet.p0.setSize(w, h);
      metaApplet.pF.add(metaApplet.p0);
      metaApplet.p1.setSize(w, (h-h2)/2+h2);
      metaApplet.p1.setBackground(Color.lightGray);
      metaApplet.p2.setSize(w, h2);
      metaApplet.entry.setSize(w, (h-h2)/2);
      metaApplet.entry.setBackground(new Color(156, 248, 248));
      metaApplet.entry.setFont(metaApplet.myFont1);
      metaApplet.message.setEditable(false);
      metaApplet.message.setSize(w, (h-h2)/2);
      metaApplet.message.setBackground(new Color(224, 204, 176));
      metaApplet.message.setFont(metaApplet.myFont3);
      metaApplet.message.setText(metaApplet.helpMessage);
      metaApplet.syntaxMessage = new MyCanvas(metaApplet, 1);
      metaApplet.syntaxMessage.setSize(200, 26);
      metaApplet.syntaxMessage.setBackground(new Color(36, 160, 160));
      metaApplet.percentStatus = new MyCanvas(metaApplet, 2);
      metaApplet.percentStatus.setSize(200, 26);
      metaApplet.percentStatus.setBackground(new Color(75, 135, 35));
      metaApplet.mma0 = new MyMouseAdapter0(metaApplet);
      metaApplet.percentStatus.addMouseListener(metaApplet.mma0);
      metaApplet.mka1 = new MyKeyAdapter1(metaApplet);
      metaApplet.mma1 = new MyMouseAdapter1(metaApplet);
      metaApplet.start = new MyButton(metaApplet.spaces(19));
      metaApplet.start.myText = "Start";
      metaApplet.start.myLength = 10;
      metaApplet.start.setBackground(new Color(0, 208, 0));
      metaApplet.start.setFont(metaApplet.myFont2);
      metaApplet.start.addKeyListener(metaApplet.mka1);
      metaApplet.start.addMouseListener(metaApplet.mma1);
      metaApplet.p2.add(metaApplet.start);
      metaApplet.mka2 = new MyKeyAdapter2(metaApplet);
      metaApplet.mma2 = new MyMouseAdapter2(metaApplet);
      metaApplet.stop = new MyButton(metaApplet.spaces(18));
      metaApplet.stop.myText = "Stop";
      metaApplet.stop.myLength = 9;
      metaApplet.stop.setBackground(new Color(224, 64, 64));
      metaApplet.stop.setFont(metaApplet.myFont2);
      metaApplet.stop.addKeyListener(metaApplet.mka2);
      metaApplet.stop.addMouseListener(metaApplet.mma2);
      metaApplet.p2.add(metaApplet.stop);
      metaApplet.mka3 = new MyKeyAdapter3(metaApplet);
      metaApplet.mma3 = new MyMouseAdapter3(metaApplet);
      metaApplet.postfixB = new MyButton(metaApplet.spaces(24));
      metaApplet.postfixB.myText = "Postfix";
      metaApplet.postfixB.myLength = 12;
      metaApplet.postfixB.setBackground(new Color(125, 175, 175));
      metaApplet.postfixB.setFont(metaApplet.myFont2);
      metaApplet.postfixB.addKeyListener(metaApplet.mka3);
      metaApplet.postfixB.addMouseListener(metaApplet.mma3);
      metaApplet.p2.add(metaApplet.postfixB);
      metaApplet.mka4 = new MyKeyAdapter4(metaApplet);
      metaApplet.mma4 = new MyMouseAdapter4(metaApplet);
      metaApplet.modelB = new MyButton(metaApplet.spaces(25));
      metaApplet.modelB.myText = "Model";
      metaApplet.modelB.myLength = 11;
      metaApplet.modelB.setBackground(new Color(64, 156, 224));
      metaApplet.modelB.setFont(metaApplet.myFont2);
      metaApplet.modelB.addKeyListener(metaApplet.mka4);
      metaApplet.modelB.addMouseListener(metaApplet.mma4);
      metaApplet.p2.add(metaApplet.modelB);
      metaApplet.mka5 = new MyKeyAdapter5(metaApplet);
      metaApplet.mma5 = new MyMouseAdapter5(metaApplet);
      metaApplet.counterexampleB = new MyButton(metaApplet.spaces(37));
      metaApplet.counterexampleB.myText = "Counterexample";
      metaApplet.counterexampleB.myLength = 17;
      metaApplet.counterexampleB.setBackground(new Color(156, 112, 160));
      metaApplet.counterexampleB.setFont(metaApplet.myFont2);
      metaApplet.counterexampleB.addKeyListener(metaApplet.mka5);
      metaApplet.counterexampleB.addMouseListener(metaApplet.mma5);
      metaApplet.p2.add(metaApplet.counterexampleB);
      metaApplet.mka6 = new MyKeyAdapter6(metaApplet);
      metaApplet.mma6 = new MyMouseAdapter6(metaApplet);
      metaApplet.reset = new MyButton(metaApplet.spaces(21));
      metaApplet.reset.myText = "Reset";
      metaApplet.reset.myLength = 10;
      metaApplet.reset.setBackground(new Color(240, 128, 176));
      metaApplet.reset.setFont(metaApplet.myFont2);
      metaApplet.reset.addKeyListener(metaApplet.mka6);
      metaApplet.reset.addMouseListener(metaApplet.mma6);
      metaApplet.p2.add(metaApplet.reset);
      metaApplet.mka7 = new MyKeyAdapter7(metaApplet);
      metaApplet.mma7 = new MyMouseAdapter7(metaApplet);
      metaApplet.paste = new MyButton(metaApplet.spaces(18));
      metaApplet.paste.myText = "Paste";
      metaApplet.paste.myLength = 9;
      metaApplet.paste.setBackground(new Color(96, 208, 208));
      metaApplet.paste.setFont(metaApplet.myFont2);
      metaApplet.paste.addKeyListener(metaApplet.mka7);
      metaApplet.paste.addMouseListener(metaApplet.mma7);
      metaApplet.p2.add(metaApplet.paste);
      metaApplet.mka8 = new MyKeyAdapter8(metaApplet);
      metaApplet.mma8 = new MyMouseAdapter8(metaApplet);
      metaApplet.clear = new MyButton(metaApplet.spaces(18));
      metaApplet.clear.myText = "Clear";
      metaApplet.clear.myLength = 9;
      metaApplet.clear.setBackground(new Color(160, 160, 224));
      metaApplet.clear.setFont(metaApplet.myFont2);
      metaApplet.clear.addKeyListener(metaApplet.mka8);
      metaApplet.clear.addMouseListener(metaApplet.mma8);
      metaApplet.p2.add(metaApplet.clear);
      metaApplet.mka9 = new MyKeyAdapter9(metaApplet);
      metaApplet.mma9 = new MyMouseAdapter9(metaApplet);
      metaApplet.scrollbar = new MyButton(metaApplet.spaces(22));
      metaApplet.scrollbar.myText = "Scrollbar";
      metaApplet.scrollbar.myLength = 12;
      metaApplet.scrollbar.setBackground(new Color(100, 150, 200));
      metaApplet.scrollbar.setFont(metaApplet.myFont2);
      metaApplet.scrollbar.addKeyListener(metaApplet.mka9);
      metaApplet.scrollbar.addMouseListener(metaApplet.mma9);
      metaApplet.p2.add(metaApplet.scrollbar);
      metaApplet.mka10 = new MyKeyAdapter10(metaApplet);
      metaApplet.mma10 = new MyMouseAdapter10(metaApplet);
      metaApplet.help = new MyButton(metaApplet.spaces(16));
      metaApplet.help.myText = "Help";
      metaApplet.help.myLength = 8;
      metaApplet.help.setBackground(new Color(240, 128, 64));
      metaApplet.help.setFont(metaApplet.myFont2);
      metaApplet.help.addKeyListener(metaApplet.mka10);
      metaApplet.help.addMouseListener(metaApplet.mma10);
      metaApplet.p2.add(metaApplet.help);
      GridBagLayout gbl = new GridBagLayout();
      GridBagConstraints gbc = new GridBagConstraints();
      metaApplet.p3 = new Panel(gbl);
      metaApplet.p3.setSize(w, h2);
      Canvas[] cs = new Canvas[5];
      for (int i = 0; i < 5; i++)
      {
         cs[i] = new Canvas();
         cs[i].setSize(100, 16);
      }
      cs[0].setSize(100, 8);
      gbc.gridy = 0;
      gbc.gridwidth = 1;
      gbl.setConstraints(cs[0], gbc);
      metaApplet.p3.add(cs[0]);
      gbc.gridy = 1;
      gbc.anchor = GridBagConstraints.WEST;
      gbl.setConstraints(cs[1], gbc);
      metaApplet.p3.add(cs[1]);
      gbc.gridwidth = 4;
      gbl.setConstraints(metaApplet.syntaxMessage, gbc);
      metaApplet.p3.add(metaApplet.syntaxMessage);
      gbc.gridwidth = 1;
      gbc.anchor = GridBagConstraints.CENTER;
      cs[2].setSize(195, 16);
      gbl.setConstraints(cs[2], gbc);
      metaApplet.p3.add(cs[2]);
      gbc.gridwidth = 4;
      gbc.anchor = GridBagConstraints.EAST;
      gbl.setConstraints(metaApplet.percentStatus, gbc);
      metaApplet.p3.add(metaApplet.percentStatus);
      gbc.gridwidth = 1;
      gbl.setConstraints(cs[3], gbc);
      metaApplet.p3.add(cs[3]);
      gbc.gridy = 2;
      gbl.setConstraints(cs[4], gbc);
      metaApplet.p3.add(cs[4]);
      metaApplet.p1.add(metaApplet.entry, "North");
      metaApplet.p1.add(metaApplet.p2, "Center");
      metaApplet.p1.add(metaApplet.p3, "South");
      metaApplet.p0.add(metaApplet.p1, "North");
      metaApplet.p0.add(metaApplet.message, "Center");
      metaApplet.pF.paintAll(metaApplet.pF.getGraphics());
      metaApplet.entry.requestFocus();
      System.gc();
   }
}


class AppletImage
{
   public Theorem metaThread;
   public Timer timerThread;
   public Frame pF = new Frame("Meta Theorem");
   public Panel p0 = new Panel(new BorderLayout()), p1 = new Panel(new
      BorderLayout()), p2 = new Panel(new FlowLayout(FlowLayout.CENTER,
      13, 16)), p3;
   public TextArea entry = new TextArea("", 15, 20, TextArea.
      SCROLLBARS_VERTICAL_ONLY), message = new TextArea(" ", 18, 20, TextArea.
      SCROLLBARS_VERTICAL_ONLY);
   public MyButton start, stop, postfixB, modelB, counterexampleB, reset, paste,
      clear, scrollbar, help;
   public MyCanvas syntaxMessage, percentStatus;
   public Font myFont1 = new Font("Monospaced", Font.BOLD, 16), myFont2 = new
      Font("SansSerif", Font.PLAIN, 16), myFont3 = new Font("SansSerif",
      Font.PLAIN, 17);
   public Color percentColor = new Color(75, 135, 35);
   public MyMouseAdapter0 mma0;
   public MyKeyAdapter1 mka1;
   public MyMouseAdapter1 mma1;
   public MyKeyAdapter2 mka2;
   public MyMouseAdapter2 mma2;
   public MyKeyAdapter3 mka3;
   public MyMouseAdapter3 mma3;
   public MyKeyAdapter4 mka4;
   public MyMouseAdapter4 mma4;
   public MyKeyAdapter5 mka5;
   public MyMouseAdapter5 mma5;
   public MyKeyAdapter6 mka6;
   public MyMouseAdapter6 mma6;
   public MyKeyAdapter7 mka7;
   public MyMouseAdapter7 mma7;
   public MyKeyAdapter8 mka8;
   public MyMouseAdapter8 mma8;
   public MyKeyAdapter9 mka9;
   public MyMouseAdapter9 mma9;
   public MyKeyAdapter10 mka10;
   public MyMouseAdapter10 mma10;
   public MyWindowAdapter mwa;
   public boolean complete = true, flip = true, on_off = true, flag_e, running;
   public long k = Long.MIN_VALUE, LEN2, lines, modelCount, counterexampleCount;
   public boolean[] boolArray = new boolean[64];
   public String helpMessage =
      "Robert Swartz\nwww.mathapplets.net\nMeta Theorem\nCopyright 2025\n\n"+
      "This program tests whether a sentence of Boolean Logic is a theorem, a "+
      "contradiction, or a contingency.  A theorem is a sentence that is true "+
      "for all variable assignments, whereas a contradiction is a sentence that"
      +" is always false; a contingency is a sentence that can be true "+
      "sometimes or false.\n\nThere are 6 logical operations:  \'and\', "+
      "\'or\', \'xor\', \'implies\', \'iff\', \'not\'.  Enter these using the "+
      "following symbols:  &  |  *  >  =  !.  Logical variables are represented"
      +" by single letters, single digits, @, or #.  The logical constants "+
      "\'true\' and \'false\' are represented by + and -.  Therefore, this "+
      "program can handle sentences with up to 64 variables.  This program "+
      "evaluates all operations from left to right; use parentheses to change "
      +"the way a logical sentence is evaluated.  Blank spaces are parsed out."+
      "\n\nFor example, the logical sentence \'(P implies Q) iff ((not P) or Q)"
      +"\' would be entered as (P > Q) = (!P | Q).\n\nThe first thing that this"
      +" program does is convert the sentence into postfix form.  Postfix form "
      +"is more efficient especially if the sentence is to be evaluated many "+
      "times.  For example, the sentence (P & (Q | R)) = ((P & Q) | (P & R)) "+
      "would be converted to P Q R | & P Q & P R & | =.  During the conversion "
      +"process, the syntax of the sentence is checked for errors.  Then, the "+
      "program goes through the truth table of the sentence, starting from the"+
      " all true case, and proceeding to all false.  It searches for 2 "+
      "different variable assignments such that one makes the sentence true "+
      "(model), and the other makes the sentence false (counterexample).  If "+
      "after going through all 2^n lines of the truth table, the program "+
      "doesn't find a model and a counterexample, then either the sentence is a"
      +" theorem if only models were found, or it's a contradiction if only "
      +"counterexamples were found.  Of course, if both a model and a "+
      "counterexample were found, the sentence is a contingency.  Here, n is "+
      "the number of variables in the sentence.\n\nWhile the applet is running,"
      +" the percentage of progress through the truth table is displayed.  "
      +"Scrolling through the truth table is possible with the Model and "+
      "Counterexample buttons; the Reset button returns the pointer to the "+
      "first line of the truth table.  It is advisable to reset the pointer "
      +"when changing scroll modes.";

   public String spaces(int size)
   {
      String text = "";
      for (int i = 1; i <= size; i++)
         text+=" ";
      return text;
   }
}


class Theorem extends Thread
{
   public AppletImage metaApplet;
   public int flag, len0, len, len2, tokens;
   public String sentence, vars0 = "", postfix = "", N = "\n\n\n", T;
   public StringTokenizer sentence2;
   public StringBuffer sentence3, stackSentence0;
   public char[] sentence4, stackSentence, vars;
   public boolean[] stack;
   public MyException myE = new MyException();

   public Theorem(AppletImage a, int n)
   {
      metaApplet = a;
      flag = n;
   }

   public void run()
   {
      long timeStamp = System.currentTimeMillis();
      metaApplet.running = true;
      metaApplet.flag_e = false;
      metaApplet.lines = -1;
      T = metaApplet.spaces(12)+"\t";
      if (flag != 2)
         metaApplet.timerThread = new Timer(metaApplet);
      else
         metaApplet.percentStatus.setText(" ");
      metaApplet.message.setText(" ");
      metaApplet.message.setFont(metaApplet.myFont1);
      metaApplet.message.setText(N+"BUSY...");
      boolean first = true, noTrue = true, noFalse = true;
      String time, assignment = "", model = "", counterexample = "", X = "";
      sentence = metaApplet.entry.getText();
      len0 = sentence.length();
      if (len0 == 0)
         myStop1();
      else
      {
         sentence2 = new StringTokenizer(sentence);
         sentence = null;
         tokens = sentence2.countTokens();
         sentence3 = new StringBuffer(len0);
         for (int i = 0; i < tokens; i++)
            sentence3.append(sentence2.nextToken());
         sentence2 = null;
         if (sentence3.length() == 0)
            myStop1();
         else
         {
            System.gc();
            sentence4 = new char[sentence3.length()];
            sentence3.getChars(0, sentence3.length(), sentence4, 0);
            sentence3 = null;
            for (int i = 0; i < sentence4.length && vars0.length() < 64; i++)
               if (isVariable(sentence4[i]) && vars0.indexOf(sentence4[i])
                  == -1)
                  vars0+=sentence4[i];
            len2 = vars0.length();
            metaApplet.LEN2 = len2;
            vars = new char[len2];
            vars0.getChars(0, len2, vars, 0);
            if (len2 <= 62)
            {
               metaApplet.lines = 1;
               for (int i = 0; i < len2; i++)
                  metaApplet.lines*=2;
               metaApplet.lines+=Long.MAX_VALUE;
            }
            else if (len2 == 64)
               metaApplet.lines = Long.MAX_VALUE;
            if (metaApplet.k == Long.MIN_VALUE)
               for (int i = 0; i < len2; i++)
                  metaApplet.boolArray[i] = false;
            stackSentence0 = new StringBuffer(sentence4.length);
            System.gc();
            try
            {
               convert(0, sentence4.length-1);
            }
            catch (MyException e)
            {
               metaApplet.flag_e = true;
            }
            if (metaApplet.running)
            {
               sentence4 = null;
               len = stackSentence0.length();
               stackSentence = new char[len];
               stackSentence0.getChars(0, len, stackSentence, 0);
               stackSentence0 = null;
               System.gc();
               stack = new boolean[len];
               metaApplet.syntaxMessage.setText("Valid Syntax");
               if (flag == 1)
               {
                  metaApplet.timerThread.start();
                  if (metaApplet.complete)
                  {
                     metaApplet.complete = false;
                     metaApplet.k = Long.MIN_VALUE;
                     for (int i = 0; i < len2; i++)
                        metaApplet.boolArray[i] = false;
                  }
                  do
                  {
                     update();
                     crunch();
                     if (metaApplet.running)
                     {
                        if (metaApplet.k == Long.MIN_VALUE)
                           first = stack[0];
                        if (stack[0])
                           noTrue = false;
                        else
                           noFalse = false;
                     }
                     metaApplet.k++;
                     if (!metaApplet.running)
                     {
                        if (metaApplet.k > Long.MIN_VALUE)
                        {
                           reverseUpdate();
                           metaApplet.k--;
                        }
                        break;
                     }
                     if ((len2 < 64 && metaApplet.k > metaApplet.lines) ||
                         (len2 == 64 && metaApplet.k == metaApplet.lines))
                        break;
                  }
                  while (metaApplet.running && (noFalse || noTrue));
                  if (len2 == 64 && metaApplet.k == metaApplet.lines)
                  {
                     update();
                     crunch();
                     if (metaApplet.running)
                     {
                        if (stack[0])
                           noTrue = false;
                        else
                           noFalse = false;
                     }
                  }
                  if (metaApplet.running)
                  {
                     metaApplet.complete = true;
                     if (!(noFalse || noTrue))
                     {
                        for (int j = 0; j < len2/4; j++)
                        {
                           for (int i = 0; i < 4; i++)
                              assignment+=vars[4*j+i]+" = "
                                 +metaApplet.boolArray[4*j+i]+T;
                           assignment+="\n";
                        }
                        for (int i = 0; i < 3; i++)
                           if (len2%4 > i)
                              assignment+=vars[len2-(len2%4-i)]+" = "
                                 +metaApplet.boolArray[len2-(len2%4-i)]+T;
                        assignment = assignment.trim();
                        model = assignment;
                        counterexample = "All variables are true.";
                        if (first)
                        {
                           model = "All variables are true.";
                           counterexample = assignment;
                        }
                        metaApplet.message.setText("\n\nThis is a contingency."
                           +"\n\nModel:\n"+model+"\n\nCounterexample:\n"
                           +counterexample);
                     }
                     else if (!noTrue)
                        metaApplet.message.setText(N+"This is a theorem.");
                     else
                        metaApplet.message.setText(N+"This is a contradiction.")
                           ;
                     time = ""+(System.currentTimeMillis()-timeStamp)/10/100.0;
                     if (time.length()-time.indexOf('.') == 2)
                        time+=0;
                     metaApplet.message.append("\n\n"+time+" seconds");
                  }
               }
               else if (flag == 2)
               {
                  metaApplet.flag_e = true;
                  for (int i = 0; i < len; i++)
                     postfix+=stackSentence[i]+" ";
                  metaApplet.message.setText(N+postfix);
               }
               else if (flag == 3 && len2 > 0)
               {
                  metaApplet.timerThread.start();
                  metaApplet.complete = false;
                  if ((len2 < 64 && metaApplet.k <= metaApplet.lines) ||
                     (len2 == 64 && metaApplet.k <  metaApplet.lines))
                  {
                     do
                     {
                        update();
                        crunch();
                        metaApplet.k++;
                        if (metaApplet.running && stack[0])
                        {
                           noTrue = false;
                           break;
                        }
                        if (!metaApplet.running)
                        {
                           if (metaApplet.k > Long.MIN_VALUE)
                           {
                              reverseUpdate();
                              metaApplet.k--;
                           }
                           break;
                        }
                     }
                     while (metaApplet.running && ((len2 < 64 && metaApplet.k <=
                        metaApplet.lines) || (len2 == 64 && metaApplet.k <
                        metaApplet.lines)));
                  }
                  if (len2 == 64 && metaApplet.k == metaApplet.lines)
                  {
                     update();
                     crunch();
                     if (metaApplet.running && stack[0])
                        noTrue = false;
                  }
                  if (metaApplet.running)
                  {
                     if (!noTrue)
                     {
                        metaApplet.modelCount++;
                        assignment = "\nModel #"+metaApplet.modelCount+":\n\n";
                        for (int j = 0; j < len2/4; j++)
                        {
                           for (int i = 0; i < 4; i++)
                              assignment+=vars[4*j+i]+" = "
                                 +metaApplet.boolArray[4*j+i]+T;
                           assignment+="\n";
                        }
                        for (int i = 0; i < 3; i++)
                           if (len2%4 > i)
                              assignment+=vars[len2-(len2%4-i)]+" = "
                                 +metaApplet.boolArray[len2-(len2%4-i)]+T;
                        metaApplet.message.setText("\n\n"+assignment.trim());
                     }
                     else if (metaApplet.k >= metaApplet.lines)
                     {
                        if (metaApplet.modelCount == 0)
                           metaApplet.message.setText(N+"No models.");
                        else
                        {
                           X = N+"No more models.\n\n"+metaApplet.modelCount;
                           if (metaApplet.modelCount == 1)
                              metaApplet.message.setText(X+" model was found.");
                           else
                              metaApplet.message.setText(X+" models were found."
                                 );
                        }
                     }
                  }
               }
               else if (flag == 4 && len2 > 0)
               {
                  metaApplet.timerThread.start();
                  metaApplet.complete = false;
                  if ((len2 < 64 && metaApplet.k <= metaApplet.lines) ||
                     (len2 == 64 && metaApplet.k <  metaApplet.lines))
                  {
                     do
                     {
                        update();
                        crunch();
                        metaApplet.k++;
                        if (metaApplet.running && !stack[0])
                        {
                           noFalse = false;
                           break;
                        }
                        if (!metaApplet.running)
                        {
                           if (metaApplet.k > Long.MIN_VALUE)
                           {
                              reverseUpdate();
                              metaApplet.k--;
                           }
                           break;
                        }
                     }
                     while (metaApplet.running && ((len2 < 64 && metaApplet.k <=
                        metaApplet.lines) || (len2 == 64 && metaApplet.k <
                        metaApplet.lines)));
                  }
                  if (len2 == 64 && metaApplet.k == metaApplet.lines)
                  {
                     update();
                     crunch();
                     if (metaApplet.running && !stack[0])
                        noFalse = false;
                  }
                  if (metaApplet.running)
                  {
                     if (!noFalse)
                     {
                        metaApplet.counterexampleCount++;
                        assignment = "\nCounterexample #"
                           +metaApplet.counterexampleCount+":\n\n";
                        for (int j = 0; j < len2/4; j++)
                        {
                           for (int i = 0; i < 4; i++)
                              assignment+=vars[4*j+i]+" = "
                                 +metaApplet.boolArray[4*j+i]+T;
                           assignment+="\n";
                        }
                        for (int i = 0; i < 3; i++)
                           if (len2%4 > i)
                              assignment+=vars[len2-(len2%4-i)]+" = "
                                 +metaApplet.boolArray[len2-(len2%4-i)]+T;
                        metaApplet.message.setText("\n\n"+assignment.trim());
                     }
                     else if (metaApplet.k >= metaApplet.lines)
                     {
                        if (metaApplet.counterexampleCount == 0)
                           metaApplet.message.setText(N+"No counterexamples.");
                        else
                        {
                           X = N+"No more counterexamples.\n\n"+
                              metaApplet.counterexampleCount;
                           if (metaApplet.counterexampleCount == 1)
                              metaApplet.message.setText(X+
                                 " counterexample was found.");
                           else
                              metaApplet.message.setText(X+
                                 " counterexamples were found.");
                        }
                     }
                  }
               }
               else if (flag == 3 && len2 == 0)
                  metaApplet.message.setText(N+"Models don't apply!");
               else
                  metaApplet.message.setText(N+"Counterexamples don't apply!");
            }
            else
               metaApplet.percentStatus.setText(" ");
         }
      }
      metaApplet.running = false;
   }

   public void convert(int pos, int end)throws MyException
   {
      int i = 0, parens = 0, nots = 0;
      boolean skip = false, error = false;
      String oper = "";
      while (pos <= end)
      {
         if (!metaApplet.running)
            throw myE;
         skip = false;
         error = true;
         nots = 0;
         parens = 0;
         while (pos <= end && sentence4[pos] == '!')
         {
            nots++;
            pos++;
         }
         if (pos > end)
            myStop2();
         if (pos != 0 && sentence4[pos-1] == '!' && !(sentence4[pos] == '(' ||
            isVariable(sentence4[pos]) || sentence4[pos] == '+' ||
            sentence4[pos] == '-'))
            myStop2();
         if (nots > 0)
            error = false;
         if (sentence4[pos] == '(')
         {
            i = pos;
            parens++;
            pos++;
            error = false;
            while (parens > 0 && pos <= end)
            {
               if (sentence4[pos] == '(')
                  parens++;
               if (sentence4[pos] == ')')
                  parens--;
               pos++;
            }
            if (parens != 0 || i == pos-2)
               myStop2();
            convert(i+1, pos-2);
            if (nots%2 == 1)
               stackSentence0.append('!');
            stackSentence0.append(oper);
            skip = true;
         }
         if (pos <= end && (isVariable(sentence4[pos]) || sentence4[pos] == '+'
            || sentence4[pos] == '-'))
         {
            if (skip)
               myStop2();
            stackSentence0.append(sentence4[pos]);
            if (nots%2 == 1)
               stackSentence0.append('!');
            stackSentence0.append(oper);
            error = false;
            pos++;
         }
         if (error)
            myStop2();
         if (pos <= end)
         {
            if (!isOperator(sentence4[pos]) || pos == end)
               myStop2();
            oper = ""+sentence4[pos];
         }
         pos++;
      }
   }

   public void crunch()
   {
      int pointer = -1;
      for (int n = 0; n < len && metaApplet.running; n++)
      {
         if (isVariable(stackSentence[n]))
            stack[++pointer] = metaApplet.boolArray[myIndex(stackSentence[n])];
         else
            switch (stackSentence[n])
            {
               case '&' ->
                  stack[--pointer] &= stack[pointer+1];
               case '|' ->
                  stack[--pointer] |= stack[pointer+1];
               case '>' ->
                  stack[--pointer] = !stack[pointer] || stack[pointer+1];
               case '=' ->
                  stack[--pointer] = !(stack[pointer] ^ stack[pointer+1]);
               case '!' ->
                  stack[pointer] = !stack[pointer];
               case '+' ->
                  stack[++pointer] = true;
               case '-' ->
                  stack[++pointer] = false;
               default ->
                  stack[--pointer] ^= stack[pointer+1];                  
            }
      }
   }

   public void update()
   {
      int i = 0;
      try
      {
         do
         {
            metaApplet.boolArray[i] = !metaApplet.boolArray[i];
            i++;
         }
         while (metaApplet.boolArray[i-1]);
      }
      catch (ArrayIndexOutOfBoundsException e)
      {
         for (i = 0; i < len2; i++)
            metaApplet.boolArray[i] = true;
      }
   }

   public void reverseUpdate()
   {
      int i = 0;
      try
      {
         do
         {
            metaApplet.boolArray[i] = !metaApplet.boolArray[i];
            i++;
         }
         while (!metaApplet.boolArray[i-1]);
      }
      catch (ArrayIndexOutOfBoundsException e)
      {
         for (i = 0; i < len2; i++)
            metaApplet.boolArray[i] = false;
      }
   }

   public int myIndex(char x)
   {
      for (int index = 0; ; index++)
         if (x == vars[index])
            return index;
   }

   public boolean isVariable(char x)
   {
      return (x >= '@' && x <= 'z') || (x >= '0' && x <= '9') || x == '#';
   }

   public boolean isOperator(char x)
   {
      return x == '&' || x == '|' || x == '>' || x == '=' || x == '*';
   }

   public void myStop1()
   {
      metaApplet.message.setText(" ");
      metaApplet.syntaxMessage.setText("Invalid Syntax!!!");
      metaApplet.flag_e = true;
      metaApplet.running = false;
   }

   public void myStop2()throws MyException
   {
      myStop1();
      throw myE;
   }
}


class MyException extends Exception{}


class Timer extends Thread
{
   public AppletImage metaApplet;

   public Timer(AppletImage a)
   {
      metaApplet = a;
   }

   public void run()
   {
      double X;
      String s;
      while (metaApplet.running && !metaApplet.flag_e)
      {
         X = ((double)(metaApplet.k+Long.MAX_VALUE+1))/Math.pow(2.0, (double)
            metaApplet.LEN2);
         if (X < 0.000001 || (X >= 1.0 && metaApplet.LEN2 == 0))
            X = 0.0;
         else
            X = Math.round(1000000.0*X)/10000.0;
         if (metaApplet.k <= metaApplet.lines)
         {
            s = ""+X;
            if (X >= 0.0001 && X < 0.001)
               s = "0.000"+s.substring(0, 1);
            else
            {
               for (int i = 1; i <= 3; i++) 
                  if ((s.substring(s.indexOf('.')+1, s.length())).length() < 4)
                     s += '0';
            }
            metaApplet.percentStatus.setText(s+"%");
         }
         else
            metaApplet.percentStatus.setText("100%");
         metaApplet.percentStatus.paint(metaApplet.percentStatus.getGraphics());
         try
         {
            sleep(333);
         }
         catch (InterruptedException e){}
      }
      if (!metaApplet.flag_e)
      {
         X = ((double)(metaApplet.k+Long.MAX_VALUE+1))/Math.pow(2.0, (double)
            metaApplet.LEN2);
         if (X < 0.000001 || (X >= 1.0 && metaApplet.LEN2 == 0))
            X = 0.0;
         else
            X = Math.round(1000000.0*X)/10000.0;
         if (metaApplet.k <= metaApplet.lines)
         {
            s = ""+X;
            if (X >= 0.0001 && X < 0.001)
               s = "0.000"+s.substring(0, 1);
            else
            {
               for (int i = 1; i <= 3; i++) 
                  if ((s.substring(s.indexOf('.')+1, s.length())).length() < 4)
                     s+='0';
            }
            metaApplet.percentStatus.setText(s+"%");
         }
         else
            metaApplet.percentStatus.setText("100%");
         metaApplet.percentStatus.clearBlock();
         metaApplet.percentStatus.paint(metaApplet.percentStatus.getGraphics());
      }
      else
         metaApplet.percentStatus.setText(" ");
   }
}


class MyCanvas extends Canvas
{
   public AppletImage metaApplet;
   public int flag;
   public String textNew = " ", textOld = " ";

   public MyCanvas(AppletImage a, int f)
   {
      metaApplet = a;
      flag = f;
   }

   public void setText(String s)
   {
      Graphics g = getGraphics();
      textNew = s;
      if (flag == 1)
      {
         g.setFont(new Font("Tahoma", Font.BOLD, 16));
         g.setColor(new Color(36, 160, 160));
         g.drawString(textOld, getSize().width/2-(int)(textOld.length()*4.1),
            getSize().height-7);
         g.setColor(Color.black);
         g.drawString(textNew, getSize().width/2-(int)(textNew.length()*4.1),
            getSize().height-7);
      }
      else if (flag == 2 && metaApplet.on_off)
      {
         g.setFont(new Font("Verdana", Font.BOLD, 16));
         g.setColor(metaApplet.percentColor);
         g.drawString(textOld, getSize().width/2-(int)(textOld.length()*5.5), 
            getSize().height-7);
         g.setColor(Color.black);
         g.drawString(textNew, getSize().width/2-(int)(textNew.length()*5.5), 
            getSize().height-7);
      }
      textOld = textNew;
   }

   public void paint(Graphics g)
   {
      if (g != null)
      {
         if (flag == 1)
         {
            g.setFont(new Font("Tahoma", Font.BOLD, 16));
            g.drawString(textNew, getSize().width/2-(int)(textNew.length()*4.1),
               getSize().height-7);
         }
         else if (flag == 2 && metaApplet.on_off)
         {
            g.setFont(new Font("Verdana", Font.BOLD, 16));
            g.drawString(textNew, getSize().width/2-(int)(textNew.length()*5.5),
               getSize().height-7);
         }
      }
   }

   public void clearBlock()
   {
      getGraphics().clearRect(0, 0, getSize().width, getSize().height);
   }
}


class MyMouseAdapter0 extends MouseAdapter
{
   public AppletImage metaApplet;

   public MyMouseAdapter0(AppletImage a)
   {
      metaApplet = a;
   }

   public void mousePressed(MouseEvent e)
   {
      if (e.getButton() == MouseEvent.BUTTON1)
      {
         metaApplet.on_off = !metaApplet.on_off;
         if (metaApplet.on_off)
            metaApplet.percentStatus.setText(metaApplet.percentStatus.textNew);
         else
            metaApplet.percentStatus.clearBlock();
      }
   }

   public void mouseEntered(MouseEvent e)
   {
      metaApplet.percentStatus.setBackground(new Color(172, 64, 120));
      metaApplet.percentColor = new Color(172, 64, 120);
   }

   public void mouseExited(MouseEvent e)
   {
      metaApplet.percentStatus.setBackground(new Color(75, 135, 35));
      metaApplet.percentColor = new Color(75, 135, 35);
   }
}


class MyButton extends Button
{
   public String myText;
   public int myLength;

   public MyButton(String mySpaces)
   {
      super(mySpaces);
   }

   public void paint(Graphics g)
   {
      g.setFont(new Font("Tahoma", Font.BOLD, 16));
      g.drawString(myText, (int)((myLength-myText.length())*5.5), 20);
   }
}


class MyKeyAdapter1 extends KeyAdapter
{
   public AppletImage metaApplet;

   public MyKeyAdapter1(AppletImage a)
   {
      metaApplet = a;
   }

   public void keyReleased(KeyEvent e)
   {
      if ((e.getKeyCode() == KeyEvent.VK_ENTER || e.getKeyCode() ==
         KeyEvent.VK_SPACE) && !metaApplet.running)
      {
         metaApplet.metaThread = new Theorem(metaApplet, 1);
         System.gc();
         metaApplet.metaThread.start();
      }
   }
}


class MyMouseAdapter1 extends MouseAdapter
{
   public AppletImage metaApplet;

   public MyMouseAdapter1(AppletImage a)
   {
      metaApplet = a;
   }

   public void mousePressed(MouseEvent e)
   {
      if (e.getButton() == MouseEvent.BUTTON1 && !metaApplet.running)
      {
         metaApplet.metaThread = new Theorem(metaApplet, 1);
         System.gc();
         metaApplet.metaThread.start();
      }
   }
}


class MyKeyAdapter2 extends KeyAdapter
{
   public AppletImage metaApplet;

   public MyKeyAdapter2(AppletImage a)
   {
      metaApplet = a;
   }

   public void keyPressed(KeyEvent e)
   {
      if (e.getKeyCode() == KeyEvent.VK_ENTER || e.getKeyCode() ==
         KeyEvent.VK_SPACE)
      {
         metaApplet.message.setText("");
         if (!metaApplet.running)
            metaApplet.syntaxMessage.setText("");
         metaApplet.running = false;
      }
   }
}


class MyMouseAdapter2 extends MouseAdapter
{
   public AppletImage metaApplet;

   public MyMouseAdapter2(AppletImage a)
   {
      metaApplet = a;
   }

   public void mousePressed(MouseEvent e)
   {
      if (e.getButton() == MouseEvent.BUTTON1)
      {
         metaApplet.message.setText("");
         if (!metaApplet.running)
            metaApplet.syntaxMessage.setText("");
         metaApplet.running = false;
      }
   }
}


class MyKeyAdapter3 extends KeyAdapter
{
   public AppletImage metaApplet;

   public MyKeyAdapter3(AppletImage a)
   {
      metaApplet = a;
   }

   public void keyReleased(KeyEvent e)
   {
      if ((e.getKeyCode() == KeyEvent.VK_ENTER || e.getKeyCode() ==
         KeyEvent.VK_SPACE) && !metaApplet.running)
      {
         metaApplet.metaThread = new Theorem(metaApplet, 2);
         System.gc();
         metaApplet.metaThread.start();
      }
   }
}


class MyMouseAdapter3 extends MouseAdapter
{
   public AppletImage metaApplet;

   public MyMouseAdapter3(AppletImage a)
   {
      metaApplet = a;
   }

   public void mousePressed(MouseEvent e)
   {
      if (e.getButton() == MouseEvent.BUTTON1 && !metaApplet.running)
      {
         metaApplet.metaThread = new Theorem(metaApplet, 2);
         System.gc();
         metaApplet.metaThread.start();
      }
   }
}


class MyKeyAdapter4 extends KeyAdapter
{
   public AppletImage metaApplet;

   public MyKeyAdapter4(AppletImage a)
   {
      metaApplet = a;
   }

   public void keyPressed(KeyEvent e)
   {
      if ((e.getKeyCode() == KeyEvent.VK_ENTER || e.getKeyCode() ==
         KeyEvent.VK_SPACE) && !metaApplet.running)
      {
         metaApplet.metaThread = new Theorem(metaApplet, 3);
         System.gc();
         metaApplet.metaThread.start();
      }
   }
}


class MyMouseAdapter4 extends MouseAdapter
{
   public AppletImage metaApplet;

   public MyMouseAdapter4(AppletImage a)
   {
      metaApplet = a;
   }

   public void mousePressed(MouseEvent e)
   {
      if (e.getButton() == MouseEvent.BUTTON1 && !metaApplet.running)
      {
         metaApplet.metaThread = new Theorem(metaApplet, 3);
         System.gc();
         metaApplet.metaThread.start();
      }
   }
}


class MyKeyAdapter5 extends KeyAdapter
{
   public AppletImage metaApplet;

   public MyKeyAdapter5(AppletImage a)
   {
      metaApplet = a;
   }

   public void keyPressed(KeyEvent e)
   {
      if ((e.getKeyCode() == KeyEvent.VK_ENTER || e.getKeyCode() ==
         KeyEvent.VK_SPACE) && !metaApplet.running)
      {
         metaApplet.metaThread = new Theorem(metaApplet, 4);
         System.gc();
         metaApplet.metaThread.start();
      }
   }
}


class MyMouseAdapter5 extends MouseAdapter
{
   public AppletImage metaApplet;

   public MyMouseAdapter5(AppletImage a)
   {
      metaApplet = a;
   }

   public void mousePressed(MouseEvent e)
   {
      if (e.getButton() == MouseEvent.BUTTON1 && !metaApplet.running)
      {
         metaApplet.metaThread = new Theorem(metaApplet, 4);
         System.gc();
         metaApplet.metaThread.start();
      }
   }
}


class MyKeyAdapter6 extends KeyAdapter
{
   public AppletImage metaApplet;

   public MyKeyAdapter6(AppletImage a)
   {
      metaApplet = a;
   }

   public void keyPressed(KeyEvent e)
   {
      if ((e.getKeyCode() == KeyEvent.VK_ENTER || e.getKeyCode() ==
         KeyEvent.VK_SPACE) && !metaApplet.running)
      {
         metaApplet.percentStatus.setText(" ");
         metaApplet.complete = true;
         metaApplet.k = Long.MIN_VALUE;
         metaApplet.modelCount = 0;
         metaApplet.counterexampleCount = 0;
      }
   }
}


class MyMouseAdapter6 extends MouseAdapter
{
   public AppletImage metaApplet;

   public MyMouseAdapter6(AppletImage a)
   {
      metaApplet = a;
   }

   public void mousePressed(MouseEvent e)
   {
      if (e.getButton() == MouseEvent.BUTTON1 && !metaApplet.running)
      {
         metaApplet.percentStatus.setText(" ");
         metaApplet.complete = true;
         metaApplet.k = Long.MIN_VALUE;
         metaApplet.modelCount = 0;
         metaApplet.counterexampleCount = 0;
      }
   }
}


class MyKeyAdapter7 extends KeyAdapter
{
   public AppletImage metaApplet;

   public MyKeyAdapter7(AppletImage a)
   {
      metaApplet = a;
   }

   public void keyPressed(KeyEvent e)
   {
      String clip = " &\n(";
      if (e.getKeyCode() == KeyEvent.VK_ENTER || e.getKeyCode() ==
         KeyEvent.VK_SPACE)
      {
         try
         {
            if (metaApplet.entry.getText().equals(""))
               clip = "(";
            metaApplet.entry.append(clip+Toolkit.getDefaultToolkit()
               .getSystemClipboard().getContents(" ").getTransferData(new
               DataFlavor(String.class, "class=java.lang.String")).toString()+
               ")");
         }
         catch (IOException e2){}
         catch (HeadlessException e3){}
         catch (UnsupportedFlavorException e4){}
      }
   }
}


class MyMouseAdapter7 extends MouseAdapter
{
   public AppletImage metaApplet;

   public MyMouseAdapter7(AppletImage a)
   {
      metaApplet = a;
   }

   public void mousePressed(MouseEvent e)
   {
      String clip = " &\n(";
      if (e.getButton() == MouseEvent.BUTTON1)
      {
         try
         {
            if (metaApplet.entry.getText().equals(""))
               clip = "(";
            metaApplet.entry.append(clip+Toolkit.getDefaultToolkit()
               .getSystemClipboard().getContents(" ").getTransferData(new
               DataFlavor(String.class, "class=java.lang.String")).toString()+
               ")");
         }
         catch (IOException e2){}
         catch (HeadlessException e3){}
         catch (UnsupportedFlavorException e4){}
      }
   }
}


class MyKeyAdapter8 extends KeyAdapter
{
   public AppletImage metaApplet;

   public MyKeyAdapter8(AppletImage a)
   {
      metaApplet = a;
   }

   public void keyPressed(KeyEvent e)
   {
      if (e.getKeyCode() == KeyEvent.VK_ENTER || e.getKeyCode() ==
         KeyEvent.VK_SPACE)
      {
         metaApplet.entry.setText(" ");
         metaApplet.entry.setText("");
      }
   }
}


class MyMouseAdapter8 extends MouseAdapter
{
   public AppletImage metaApplet;

   public MyMouseAdapter8(AppletImage a)
   {
      metaApplet = a;
   }

   public void mousePressed(MouseEvent e)
   {
      if (e.getButton() == MouseEvent.BUTTON1)
      {
         metaApplet.entry.setText(" ");
         metaApplet.entry.setText("");
      }
   }
}


class MyKeyAdapter9 extends KeyAdapter
{
   public AppletImage metaApplet;

   public MyKeyAdapter9(AppletImage a)
   {
      metaApplet = a;
   }

   public void keyReleased(KeyEvent e)
   {
      TextArea X = metaApplet.entry;
      if (e.getKeyCode() == KeyEvent.VK_ENTER || e.getKeyCode() ==
         KeyEvent.VK_SPACE)
      {
         if (metaApplet.flip)
            metaApplet.entry = new TextArea(X.getText(), 15, 20,
               TextArea.SCROLLBARS_BOTH);
         else
            metaApplet.entry = new TextArea(X.getText(), 15, 20,
               TextArea.SCROLLBARS_VERTICAL_ONLY);
         metaApplet.flip = !metaApplet.flip;
         metaApplet.entry.setSize(1240, 324);
         metaApplet.entry.setBackground(new Color(156, 248, 248));
         metaApplet.entry.setFont(metaApplet.myFont1);
         metaApplet.pF.removeAll();
         metaApplet.p0.removeAll();
         metaApplet.p1.removeAll();
         metaApplet.p1.add(metaApplet.entry, "North");
         metaApplet.p1.add(metaApplet.p2, "Center");
         metaApplet.p1.add(metaApplet.p3, "South");
         metaApplet.p0.add(metaApplet.p1, "North");
         metaApplet.p0.add(metaApplet.message, "Center");
         metaApplet.pF.add(metaApplet.p0);
         metaApplet.pF.paintAll(metaApplet.pF.getGraphics());
         metaApplet.scrollbar.requestFocus();
      }
   }
}


class MyMouseAdapter9 extends MouseAdapter
{
   public AppletImage metaApplet;

   public MyMouseAdapter9(AppletImage a)
   {
      metaApplet = a;
   }

   public void mousePressed(MouseEvent e)
   {
      TextArea X = metaApplet.entry;
      if (e.getButton() == MouseEvent.BUTTON1)
      {
         if (metaApplet.flip)
            metaApplet.entry = new TextArea(X.getText(), 15, 20,
               TextArea.SCROLLBARS_BOTH);
         else
            metaApplet.entry = new TextArea(X.getText(), 15, 20,
               TextArea.SCROLLBARS_VERTICAL_ONLY);
         metaApplet.flip = !metaApplet.flip;
         metaApplet.entry.setSize(1240, 324);
         metaApplet.entry.setBackground(new Color(156, 248, 248));
         metaApplet.entry.setFont(metaApplet.myFont1);
         metaApplet.pF.removeAll();
         metaApplet.p0.removeAll();
         metaApplet.p1.removeAll();
         metaApplet.p1.add(metaApplet.entry, "North");
         metaApplet.p1.add(metaApplet.p2, "Center");
         metaApplet.p1.add(metaApplet.p3, "South");
         metaApplet.p0.add(metaApplet.p1, "North");
         metaApplet.p0.add(metaApplet.message, "Center");
         metaApplet.pF.add(metaApplet.p0);
         metaApplet.pF.paintAll(metaApplet.pF.getGraphics());
         metaApplet.scrollbar.requestFocus();
      }
   }
}


class MyKeyAdapter10 extends KeyAdapter
{
   public AppletImage metaApplet;

   public MyKeyAdapter10(AppletImage a)
   {
      metaApplet = a;
   }

   public void keyReleased(KeyEvent e)
   {
      if ((e.getKeyCode() == KeyEvent.VK_ENTER || e.getKeyCode() ==
         KeyEvent.VK_SPACE) && !metaApplet.running)
      {
         metaApplet.message.setText(" ");
         metaApplet.message.setFont(metaApplet.myFont3);
         metaApplet.message.setText(metaApplet.helpMessage);
      }
   }
}


class MyMouseAdapter10 extends MouseAdapter
{
   public AppletImage metaApplet;

   public MyMouseAdapter10(AppletImage a)
   {
      metaApplet = a;
   }

   public void mousePressed(MouseEvent e)
   {
      if (e.getButton() == MouseEvent.BUTTON1 && !metaApplet.running)
      {
         metaApplet.message.setText(" ");
         metaApplet.message.setFont(metaApplet.myFont3);
         metaApplet.message.setText(metaApplet.helpMessage);
      }
   }
}


class MyWindowAdapter extends WindowAdapter
{
   public AppletImage metaApplet;

   public MyWindowAdapter(AppletImage a)
   {
      metaApplet = a;
   }

   public void windowClosing(WindowEvent e)
   {
      metaApplet.running = false;
      metaApplet.pF.dispose();
   }
}