public static Cons nextEquivalentSelectionPattern(AbstractPropositionsIterator self) {
    { Cons pattern = self.selectionPattern;
      LogicObject keywithequivalents = null;
      Cons equivalentsstack = self.equivalentsStack;
      LogicObject newskolem = null;
      Cons equivalentskolems = null;

      if (equivalentsstack == null) {
        keywithequivalents = Logic.findSelectionKeyWithEquivalents(pattern);
        if (keywithequivalents != null) {
          equivalentskolems = keywithequivalents.variableValueInverse();
          equivalentsstack = Cons.cons(equivalentskolems, Stella.NIL);
        }
      }
      if (equivalentsstack == null) {
        self.equivalentsStack = Stella.NIL;
        return (null);
      }
      if (equivalentsstack == Stella.NIL) {
        return (null);
      }
      equivalentskolems = ((Cons)(equivalentsstack.value));
      newskolem = ((LogicObject)(equivalentskolems.value));
      equivalentsstack.firstSetter(equivalentskolems.rest);
      if (equivalentsstack.value == Stella.NIL) {
        equivalentsstack = equivalentsstack.rest;
      }
      if (!(newskolem.variableValueInverse() == Stella.NIL)) {
        equivalentsstack = Cons.cons(newskolem.variableValueInverse(), equivalentsstack);
      }
      self.equivalentsStack = equivalentsstack;
      if (keywithequivalents == null) {
        keywithequivalents = Logic.findSelectionKeyWithEquivalents(pattern);
      }
      return (((Cons)(Stella_Object.substituteConsTree(((Cons)(Stella_Object.copyConsTree(pattern))), newskolem, keywithequivalents))));
    }
  }