public static void normalizeAndProposition(Proposition self) {
    { Cons otherprops = Stella.NIL;
      boolean conjoinP = false;
      Cons existsvariables = Stella.NIL;

      { Stella_Object arg = null;
        Vector vector000 = self.arguments;
        int index000 = 0;
        int length000 = vector000.length();

        for (;index000 < length000; index000 = index000 + 1) {
          arg = (vector000.theArray)[index000];
          if (Logic.variableP(arg)) {
            { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

              { Object old$PrintreadablyP$000 = Stella.$PRINTREADABLYp$.get();

                try {
                  Native.setBooleanSpecial(Stella.$PRINTREADABLYp$, true);
                  stream000.nativeStream.println("ERROR: Can't yet handle propositional variables within conjunctions.");
                  Logic.helpSignalPropositionError(stream000, Logic.KWD_ERROR);

                } finally {
                  Stella.$PRINTREADABLYp$.set(old$PrintreadablyP$000);
                }
              }
              throw ((PropositionError)(PropositionError.newPropositionError(stream000.theStringReader()).fillInStackTrace()));
            }
          }
          { Proposition conjunct = ((Proposition)(arg));

            Proposition.normalizeProposition(conjunct);
            { Keyword testValue000 = conjunct.kind;

              if (testValue000 == Logic.KWD_EXISTS) {
                { PatternVariable v = null;
                  Vector vector001 = ((Vector)(KeyValueList.dynamicSlotValue(conjunct.dynamicSlots, Logic.SYM_LOGIC_IO_VARIABLES, null)));
                  int index001 = 0;
                  int length001 = vector001.length();
                  Cons collect000 = null;

                  for (;index001 < length001; index001 = index001 + 1) {
                    v = ((PatternVariable)((vector001.theArray)[index001]));
                    { boolean foundP000 = false;

                      { PatternVariable var = null;
                        Cons iter000 = existsvariables;

                        loop002 : for (;!(iter000 == Stella.NIL); iter000 = iter000.rest) {
                          var = ((PatternVariable)(iter000.value));
                          if (Symbol.variableEqlP(var.skolemName, v.skolemName)) {
                            foundP000 = true;
                            break loop002;
                          }
                        }
                      }
                      if (foundP000) {
                        PatternVariable.renameLogicVariableApart(v, true);
                      }
                    }
                    if (collect000 == null) {
                      {
                        collect000 = Cons.cons(v, Stella.NIL);
                        if (existsvariables == Stella.NIL) {
                          existsvariables = collect000;
                        }
                        else {
                          Cons.addConsToEndOfConsList(existsvariables, collect000);
                        }
                      }
                    }
                    else {
                      {
                        collect000.rest = Cons.cons(v, Stella.NIL);
                        collect000 = collect000.rest;
                      }
                    }
                  }
                }
                otherprops = Cons.cons((conjunct.arguments.theArray)[0], otherprops);
                conjoinP = true;
              }
              else if (testValue000 == Logic.KWD_AND) {
                otherprops = Cons.cons(conjunct, otherprops);
                conjoinP = true;
              }
              else if (testValue000 == Logic.KWD_CONSTANT) {
                if (conjunct.operator == Logic.SGT_STELLA_TRUE) {
                  conjoinP = true;
                  otherprops = Cons.cons(conjunct, otherprops);
                }
                else if (conjunct.operator == Logic.SGT_STELLA_FALSE) {
                  Proposition.overlayWithConstantProposition(self, Logic.FALSE_PROPOSITION);
                  return;
                }
              }
              else {
                { boolean testValue001 = false;

                  testValue001 = !conjoinP;
                  if (testValue001) {
                    { boolean foundP001 = false;

                      { Stella_Object prop = null;
                        Cons iter001 = otherprops;

                        loop003 : for (;!(iter001 == Stella.NIL); iter001 = iter001.rest) {
                          prop = iter001.value;
                          if (Proposition.duplicateAndOrArgumentsP(((Proposition)(prop)), conjunct)) {
                            foundP001 = true;
                            break loop003;
                          }
                        }
                      }
                      testValue001 = foundP001;
                    }
                  }
                  if (testValue001) {
                    conjoinP = true;
                  }
                  else {
                    otherprops = Cons.cons(conjunct, otherprops);
                  }
                }
              }
            }
          }
        }
      }
      otherprops = otherprops.reverse();
      if (!(existsvariables == Stella.NIL)) {
        { Proposition existsproposition = Logic.createProposition(Logic.SYM_STELLA_EXISTS, 1);

          KeyValueList.setDynamicSlotValue(existsproposition.dynamicSlots, Logic.SYM_LOGIC_IO_VARIABLES, Logic.copyConsListToVariablesVector(existsvariables), null);
          (existsproposition.arguments.theArray)[0] = (Logic.conjoinPropositions(otherprops));
          Proposition.overlayProposition(self, existsproposition);
        }
        return;
      }
      if (conjoinP ||
          (otherprops.length() <= 1)) {
        Proposition.overlayProposition(self, Logic.conjoinPropositions(otherprops));
      }
    }
  }