public static boolean propositionLessThanP(Proposition p1, Proposition p2) {
    { String operator1 = p1.operator.symbolName;
      String operator2 = p2.operator.symbolName;
      Vector arguments1 = p1.arguments;
      Vector arguments2 = p2.arguments;
      int end1 = arguments1.length() - 1;
      int end2 = arguments2.length() - 1;
      Stella_Object a1 = null;
      Stella_Object a2 = null;

      if (Stella.stringLessP(operator1, operator2)) {
        return (true);
      }
      if (Stella.stringLessP(operator2, operator1)) {
        return (false);
      }
      { int i1 = Stella.NULL_INTEGER;
        int iter000 = 0;
        int upperBound000 = end1;
        boolean unboundedP000 = upperBound000 == Stella.NULL_INTEGER;
        int i2 = Stella.NULL_INTEGER;
        int iter001 = 0;
        int upperBound001 = end2;
        boolean unboundedP001 = upperBound001 == Stella.NULL_INTEGER;

        for (;(unboundedP000 ||
                  (iter000 <= upperBound000)) &&
                  (unboundedP001 ||
                   (iter001 <= upperBound001)); iter000 = iter000 + 1, iter001 = iter001 + 1) {
          i1 = iter000;
          i2 = iter001;
          a1 = (arguments1.theArray)[i1];
          a2 = (arguments2.theArray)[i2];
          if ((i1 == end1) &&
              ((i2 == end2) &&
               (Logic.functionOutputSkolemP(a1) &&
                (Logic.functionOutputSkolemP(a2) &&
                 ((((Skolem)(a1)).definingProposition == p1) &&
                  ((((Skolem)(a2)).definingProposition == p2) &&
                   (Stella_Object.eqlP(Logic.valueOf(a1), a1) &&
                    Stella_Object.eqlP(Logic.valueOf(a2), a2)))))))) {
            return (false);
          }
          if (Logic.logicFormLessP(a1, a2)) {
            return (true);
          }
          else {
            if (Logic.logicFormLessP(a2, a1)) {
              return (false);
            }
          }
        }
      }
      return (end1 < end2);
    }
  }