public static Cons leastGeneralGeneralization(Cons clause1, Cons clause2) {
    { List matches = List.newList();
      Cons probe = Stella.NIL;
      Symbol operator = null;
      List bindings = List.newList();
      Cons newClause = Stella.NIL;
      List vars1 = Logic.getVariablesFromConsPropositions(Cons.consList(Cons.cons(clause1, Stella.NIL)));
      List vars2 = Logic.getVariablesFromConsPropositions(Cons.consList(Cons.cons(clause2, Stella.NIL)));
      boolean notP = false;
      Symbol var = null;
      Cons result = Stella.NIL;

      { Symbol var000 = null;
        Cons iter000 = vars1.theConsList;
        int i = Stella.NULL_INTEGER;
        int iter001 = 0;

        for (;!(iter000 == Stella.NIL); iter000 = iter000.rest, iter001 = iter001 + 1) {
          var000 = ((Symbol)(iter000.value));
          i = iter001;
          if (!(var000 == Logic.SYM_LOGIC_pY)) {
            clause1 = ((Cons)(Stella_Object.substituteConsTree(clause1, var000, Symbol.internSymbol("?A" + Native.stringify(IntegerWrapper.wrapInteger(i))))));
          }
        }
      }
      { Symbol var000 = null;
        Cons iter002 = vars2.theConsList;
        int i = Stella.NULL_INTEGER;
        int iter003 = 0;

        for (;!(iter002 == Stella.NIL); iter002 = iter002.rest, iter003 = iter003 + 1) {
          var000 = ((Symbol)(iter002.value));
          i = iter003;
          if (!(var000 == Logic.SYM_LOGIC_pY)) {
            clause2 = ((Cons)(Stella_Object.substituteConsTree(clause1, var000, Symbol.internSymbol("?B" + Native.stringify(IntegerWrapper.wrapInteger(i))))));
          }
        }
      }
      Native.setIntSpecial(Logic.$BOTTOM_UP_VARIABLE_COUNTER$, 0);
      { Cons clause = null;
        Cons iter004 = ((Cons)(Stella_Object.copyConsTree(clause1)));

        for (;!(iter004 == Stella.NIL); iter004 = iter004.rest) {
          clause = ((Cons)(iter004.value));
          if (clause.value == Logic.SYM_STELLA_NOT) {
            {
              notP = true;
              probe = ((Cons)(clause.rest.value));
            }
          }
          else {
            {
              notP = false;
              probe = clause;
            }
          }
          operator = ((Symbol)(probe.value));
          matches = List.newList();
          { Cons potentialMatch = null;
            Cons iter005 = ((Cons)(Stella_Object.copyConsTree(clause2)));

            for (;!(iter005 == Stella.NIL); iter005 = iter005.rest) {
              potentialMatch = ((Cons)(iter005.value));
              if (notP &&
                  ((potentialMatch.value == Logic.SYM_STELLA_NOT) &&
                   (((Cons)(potentialMatch.rest.value)).value == operator))) {
                matches.push(((Cons)(potentialMatch.rest.value)));
              }
              if ((!notP) &&
                  (potentialMatch.value == operator)) {
                matches.push(potentialMatch);
              }
            }
          }
          if (!matches.emptyP()) {
            { Cons match = null;
              Cons iter006 = matches.theConsList;

              for (;!(iter006 == Stella.NIL); iter006 = iter006.rest) {
                match = ((Cons)(iter006.value));
                if ((operator == Logic.SYM_STELLA_g) ||
                    ((operator == Logic.SYM_STELLA_l) ||
                     ((operator == Logic.SYM_STELLA_ge) ||
                      (operator == Logic.SYM_STELLA_el)))) {
                  newClause = Logic.generalizeInequality(probe, match, bindings);
                }
                else {
                  newClause = Cons.cons(operator, Stella.NIL);
                  { Stella_Object arg1 = null;
                    Cons iter007 = probe.rest;
                    Stella_Object arg2 = null;
                    Cons iter008 = match.rest;

                    for (;(!(iter007 == Stella.NIL)) &&
                              (!(iter008 == Stella.NIL)); iter007 = iter007.rest, iter008 = iter008.rest) {
                      arg1 = iter007.value;
                      arg2 = iter008.value;
                      if (!Stella_Object.equalConsTreesP(arg1, arg2)) {
                        {
                          var = ((Symbol)(Logic.lookupVariableInBindings(arg1, arg2, bindings)));
                          if (var == null) {
                            var = Symbol.internSymbol("?X" + Native.stringify(IntegerWrapper.wrapInteger(((Integer)(Logic.$BOTTOM_UP_VARIABLE_COUNTER$.get())).intValue())));
                            if (!Logic.eitherNumbersP(arg1, arg2)) {
                              bindings.push(Cons.consList(Cons.cons(arg1, Cons.cons(arg2, Cons.cons(var, Stella.NIL)))));
                            }
                            Native.setIntSpecial(Logic.$BOTTOM_UP_VARIABLE_COUNTER$, ((Integer)(Logic.$BOTTOM_UP_VARIABLE_COUNTER$.get())).intValue() + 1);
                          }
                          newClause = Cons.cons(var, newClause);
                        }
                      }
                      else {
                        newClause = Cons.cons(arg1, newClause);
                      }
                    }
                  }
                  newClause = newClause.reverse();
                }
                if (notP) {
                  newClause = Cons.list$(Cons.cons(Logic.SYM_STELLA_NOT, Cons.cons(newClause, Cons.cons(Stella.NIL, Stella.NIL))));
                }
                result = Cons.cons(newClause, result);
              }
            }
          }
        }
      }
      return (Logic.removeRedundantClauses(result.reverse()));
    }
  }